Theorem map_app_composition

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ map g Y Z, hypo.
03. 3 ⊢ x ∈ X, hypo.
04. 1, 2 ⊢ map (g ∘ f) X Z, composition_is_map 1 2.
05. 1, 3 ⊢ ∃y. y ∈ Y ∧ y = app f x, map_app_exists 1 3.
06. 6 ⊢ y ∈ Y ∧ y = app f x, hypo.
07. 6 ⊢ y ∈ Y, conj_eliml 6.
08. 6 ⊢ y = app f x, conj_elimr 6.
09. ⊢ app g y = app g y, eq_refl.
10. 6 ⊢ app g (app f x) = app g y,
  eq_subst 8 9, P t ↔ app g t = app g y.
11. 1, 3, 6 ⊢ (x, y) ∈ f, map_app_elim 1 3 8.
12. 2, 6 ⊢ (y, app g (app f x)) ∈ g, map_app_elim 2 7 10.
13. 1, 2, 3, 6 ⊢ (x, app g (app f x)) ∈ g ∘ f, composition_intro 11 12.
14. 1, 2, 3, 6 ⊢ app g (app f x) = app (g ∘ f) x, map_app_intro 4 13.
15. 1, 2, 3, 6 ⊢ app (g ∘ f) x = app g (app f x), eq_symm 14.
16. 1, 2, 3 ⊢ app (g ∘ f) x = app g (app f x), ex_elim 5 15.
map_app_composition. ⊢ map f X Y → map g Y Z → x ∈ X →
  app (g ∘ f) x = app g (app f x), subj_intro_iii 16.

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