Theorem composition_sur_sur_is_sur

Proof
01. 1 ⊢ sur f X Y, hypo.
02. 2 ⊢ sur g Y Z, hypo.
03. 1 ⊢ map f X Y, sur_is_map 1.
04. 2 ⊢ map g Y Z, sur_is_map 2.
05. 1, 2 ⊢ map (g ∘ f) X Z, composition_is_map 3 4.
06. 1 ⊢ rng f = Y, sur_elim 1.
07. 2 ⊢ rng g = Z, sur_elim 2.
08. 8 ⊢ z ∈ Z, hypo.
09. 2, 8 ⊢ z ∈ rng g, eq_subst_rev 7 8.
10. 2, 8 ⊢ ∃y. (y, z) ∈ g, rng_elim 9.
11. 11 ⊢ (y, z) ∈ g, hypo.
12. 11 ⊢ y ∈ dom g, dom_intro 11.
13. 2 ⊢ function g ∧ dom g = Y ∧ rng g ⊆ Z, map_unfold 4.
14. 2 ⊢ dom g = Y, conj_elimlr 13.
15. 2, 11 ⊢ y ∈ Y, eq_subst 14 12, P u ↔ y ∈ u.
16. 1, 2, 11 ⊢ y ∈ rng f, eq_subst_rev 6 15.
17. 1, 2, 11 ⊢ ∃x. (x, y) ∈ f, rng_elim 16.
18. 18 ⊢ (x, y) ∈ f, hypo.
19. 11, 18 ⊢ (x, z) ∈ g ∘ f, composition_intro 18 11.
20. 11, 18 ⊢ z ∈ rng (g ∘ f), rng_intro 19.
21. 1, 2, 11 ⊢ z ∈ rng (g ∘ f), ex_elim 17 20.
22. 1, 2, 8 ⊢ z ∈ rng (g ∘ f), ex_elim 10 21.
23. 1, 2 ⊢ z ∈ Z → z ∈ rng (g ∘ f), subj_intro 22.
24. 1, 2 ⊢ ∀z. z ∈ Z → z ∈ rng (g ∘ f), uq_intro 23.
25. 1, 2 ⊢ Z ⊆ rng (g ∘ f), incl_intro 24.
26. 1, 2 ⊢ sur (g ∘ f) X Z, sur_intro 5 25.
composition_sur_sur_is_sur. ⊢ sur f X Y → sur g Y Z →
  sur (g ∘ f) X Z, subj_intro_ii 26.

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