Theorem map_union

Proof
01. 1 ⊢ map f X1 Y1, hypo.
02. 2 ⊢ map g X2 Y2, hypo.
03. 3 ⊢ X1 ∩ X2 = ∅, hypo.
04. 1 ⊢ function f ∧ dom f = X1 ∧ rng f ⊆ Y1, map_unfold 1.
05. 2 ⊢ function g ∧ dom g = X2 ∧ rng g ⊆ Y2, map_unfold 2.
06. 1 ⊢ function f, conj_elimll 4.
07. 1 ⊢ dom f = X1, conj_elimlr 4.
08. 1 ⊢ rng f ⊆ Y1, conj_elimr 4.
09. 2 ⊢ function g, conj_elimll 5.
10. 2 ⊢ dom g = X2, conj_elimlr 5.
11. 2 ⊢ rng g ⊆ Y2, conj_elimr 5.
12. 1, 3 ⊢ dom f ∩ X2 = ∅, eq_subst_rev 7 3.
13. 1, 2, 3 ⊢ dom f ∩ dom g = ∅, eq_subst_rev 10 12.
14. 1, 2, 3 ⊢ function (f ∪ g), function_union 6 9 13.
15. ⊢ dom (f ∪ g) = dom f ∪ dom g, dom_union.
16. 1 ⊢ dom (f ∪ g) = X1 ∪ dom g, eq_subst 7 15,
  P X ↔ dom (f ∪ g) = X ∪ dom g.
17. 1, 2 ⊢ dom (f ∪ g) = X1 ∪ X2, eq_subst 10 16,
  P X ↔ dom (f ∪ g) = X1 ∪ X.
18. ⊢ rng (f ∪ g) = rng f ∪ rng g, rng_union.
19. ⊢ rng (f ∪ g) ⊆ rng f ∪ rng g, incl_from_eq 18.
20. 1, 2 ⊢ rng f ∪ rng g ⊆ Y1 ∪ Y2, union_incl_in_union 8 11.
21. 1, 2 ⊢ rng (f ∪ g) ⊆ Y1 ∪ Y2, incl_trans 19 20.
22. 1, 2, 3 ⊢ map (f ∪ g) (X1 ∪ X2) (Y1 ∪ Y2), map_intro 14 17 21.
map_union. ⊢ map f X1 Y1 → map g X2 Y2 → X1 ∩ X2 = ∅ →
  map (f ∪ g) (X1 ∪ X2) (Y1 ∪ Y2), subj_intro_iii 22.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.