Let f, X, X' and Y be given.
Assume HX: total_function_on f X Y.
Assume HdomX: graph_domain_subset f X.
Assume HX': total_function_on f X' Y.
Assume HdomX': graph_domain_subset f X'.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X.
We prove the intermediate claim Hex: ∃y : set, (x,y) ∈ f.
An exact proof term for the current goal is (iffEL (x ∈ X) (∃y : set, (x,y) ∈ f) (total_function_on_domain_iff_exists_pair f X Y x HX HdomX) Hx).
Apply Hex to the current goal.
Let y be given.
Assume Hxy: (x,y) ∈ f.
An exact proof term for the current goal is (HdomX' x y Hxy).
Let x be given.
Assume Hx: x ∈ X'.
We prove the intermediate claim Hex: ∃y : set, (x,y) ∈ f.
An exact proof term for the current goal is (iffEL (x ∈ X') (∃y : set, (x,y) ∈ f) (total_function_on_domain_iff_exists_pair f X' Y x HX' HdomX') Hx).
Apply Hex to the current goal.
Let y be given.
Assume Hxy: (x,y) ∈ f.
An exact proof term for the current goal is (HdomX x y Hxy).
∎