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 prove the intermediate claim Hrf: graph_range_subset f Y.
An exact proof term for the current goal is (graph_range_subset_from_total_functional A Y f Hdomf Htotf Hfunf).
We prove the intermediate claim Hrg: graph_range_subset g Y.
An exact proof term for the current goal is (graph_range_subset_from_total_functional B Y g Hdomg Htotg Hfung).
We prove the intermediate claim Hrfg: graph_range_subset (f ∪ g) Y.
An exact proof term for the current goal is (graph_range_subset_binunion f g Y Hrf Hrg).
We prove the intermediate claim Htotfg: ∀x : set, x ∈ (A ∪ B) → ∃y : set, y ∈ Y ∧ (x,y) ∈ (f ∪ g).
Let x be given.
Assume Hx: x ∈ (A ∪ B).
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)).
An exact proof term for the current goal is (function_on_from_totality_and_range (A ∪ B) Y (f ∪ g) Htotfg Hrfg).
∎