Let A, B, Y, f, g and x 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.

Assume HxA: x ∈ A.

We prove the intermediate claim Hpairf: (x,apply_fun f x) ∈ f.

An exact proof term for the current goal is (total_function_on_apply_fun_in_graph f A Y x Htotf HxA).

We prove the intermediate claim HpairU: (x,apply_fun f x) ∈ (f ∪ g).

An exact proof term for the current goal is (binunionI1 f g (x,apply_fun f x) Hpairf).

We prove the intermediate claim HfunU: functional_graph (f ∪ g).

An exact proof term for the current goal is (functional_graph_union_disjoint_domains A B f g Hdisj Hdomf Hdomg Hfunf Hfung).

An exact proof term for the current goal is (functional_graph_apply_fun_eq (f ∪ g) x (apply_fun f x) HfunU HpairU).

∎