suffices f.graph = g.graph from by
  cases f
  cases this
  rfl
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f = g
V : Type u_1
inst✝ : Zermelo V
r x y z a b c : V
f g : a ⟶ b
h : ∀ (x : V), x ∈ a → apply f.graph x = apply g.graph x
⊢ f.graph = g.graph