diff --git a/DynamicalSystems/InputOutput/ClosedLoop.lean b/DynamicalSystems/InputOutput/ClosedLoop.lean
index b0852b5..513cce9 100644
--- a/DynamicalSystems/InputOutput/ClosedLoop.lean
+++ b/DynamicalSystems/InputOutput/ClosedLoop.lean
@@ -279,11 +279,48 @@ theorem comp_inputStateLp_mapProdLp (hG₁ : Function.graph G₁ = loop.topRel)
 
 end mem_loop
 
-proof_wanted isGraph_inputOutput (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph)
-    (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph
-
-proof_wanted isGraph_inputState (h_topRel : loop.topRel.IsGraph) (h_botRel : loop.botRel.IsGraph)
-    (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph
+/-- If the map from inputs to states is a graph, then the map from inputs to outputs is also a
+graph. -/
+theorem isGraph_inputOutput (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph)
+    (h : loop.inputState.IsGraph) : loop.inputOutput.IsGraph := by
+  intro e
+  obtain ⟨u, hu, hu_uniq⟩ := h e
+  refine ⟨fun a ↦ ((u a).2 - (e a).2, (e a).1 - (u a).1), ?_, ?_⟩
+  · dsimp only
+    rw [mem_inputOutput]
+    constructor
+    · convert hu.1 using 2
+      · ext a; simp
+      · ext a; simp
+    · convert hu.2 using 2
+      · ext a; simp
+      · ext a; simp
+  · intro y' hy'
+    have hu' := mem_inputState_of_mem_inputOutput hy'
+    have heq := hu_uniq _ hu'
+    rw [← heq]
+    ext a <;> simp
+
+/-- If the map from inputs to outputs is a graph, then the map from inputs to states is also a
+graph. -/
+theorem isGraph_inputState (_h_topRel : loop.topRel.IsGraph) (_h_botRel : loop.botRel.IsGraph)
+    (h : loop.inputOutput.IsGraph) : loop.inputState.IsGraph := by
+  intro e
+  obtain ⟨y, hy, hy_uniq⟩ := h e
+  refine ⟨e - (fun x ↦ (x.2, -x.1)) ∘ y, mem_inputState_of_mem_inputOutput hy, ?_⟩
+  intro u' hu'
+  have hy' : (e, fun a ↦ ((u' a).2 - (e a).2, (e a).1 - (u' a).1)) ∈ loop.inputOutput := by
+    rw [mem_inputOutput]
+    constructor
+    · convert hu'.1 using 2
+      · ext a; simp
+      · ext a; simp
+    · convert hu'.2 using 2
+      · ext a; simp
+      · ext a; simp
+  have heq := hy_uniq _ hy'
+  rw [← heq]
+  ext a <;> simp
 
 variable [MeasurableSpace α] {μ : Measure α}