Let A, B, Y, f and g be given.
Assume Hdisj: A ∩ B = Empty.
Assume Hdomf: graph_domain_subset f A.
Assume Hdomg: graph_domain_subset g B.
Assume Htotf: total_function_on f A Y.
Assume Htotg: total_function_on g B Y.
Assume Hfunf: functional_graph f.
Assume Hfung: functional_graph g.
We will prove function_on (f ∪ g) (A ∪ B) Y ∧ ∀x : set, x ∈ (A ∪ B) → ∃y : set, y ∈ Y ∧ (x,y) ∈ (f ∪ g).
Apply andI to the current goal.
An exact proof term for the current goal is (function_union_on_disjoint_total_functional A B Y f g Hdisj Hdomf Hdomg Htotf Htotg Hfunf Hfung).
Let x be given.
Assume Hx: x ∈ (A ∪ B).
We will prove ∃y : set, y ∈ Y ∧ (x,y) ∈ (f ∪ g).
Apply (binunionE A B x Hx) to the current goal.
Assume HxA: x ∈ A.
Apply (total_function_on_totality f A Y Htotf x HxA) to the current goal.
Let y be given.
Assume Hy: y ∈ Y ∧ (x,y) ∈ f.
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (y ∈ Y) ((x,y) ∈ f) Hy).
An exact proof term for the current goal is (binunionI1 f g (x,y) (andER (y ∈ Y) ((x,y) ∈ f) Hy)).
Assume HxB: x ∈ B.
Apply (total_function_on_totality g B Y Htotg x HxB) to the current goal.
Let y be given.
Assume Hy: y ∈ Y ∧ (x,y) ∈ g.
We use y to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (y ∈ Y) ((x,y) ∈ g) Hy).
An exact proof term for the current goal is (binunionI2 f g (x,y) (andER (y ∈ Y) ((x,y) ∈ g) Hy)).
∎