Let X, A, B, Y, Tx, Ty, f and g be given.

Assume HTx: topology_on X Tx.

Assume HA: A ∈ Tx.

Assume HB: B ∈ Tx.

Assume Hdisj: A ∩ B = Empty.

Assume Hdomf: graph_domain_subset f A.

Assume Hdomg: graph_domain_subset g B.

Assume Hfunf: functional_graph f.

Assume Hfung: functional_graph g.

Assume Hf: continuous_map_total A (subspace_topology X Tx A) Y Ty f.

Assume Hg: continuous_map_total B (subspace_topology X Tx B) Y Ty g.

We will prove continuous_map (A ∪ B) (subspace_topology X Tx (A ∪ B)) Y Ty (f ∪ g).

We prove the intermediate claim Htot: continuous_map_total (A ∪ B) (subspace_topology X Tx (A ∪ B)) Y Ty (f ∪ g).

An exact proof term for the current goal is (pasting_lemma_total_functional X A B Y Tx Ty f g HTx HA HB Hdisj Hdomf Hdomg Hfunf Hfung Hf Hg).

An exact proof term for the current goal is (continuous_map_total_imp (A ∪ B) (subspace_topology X Tx (A ∪ B)) Y Ty (f ∪ g) Htot).

∎