Theorem composition_bij_bij_is_bij

Proof
01. 1 ⊢ bij f X Y, hypo.
02. 2 ⊢ bij g Y Z, hypo.
03. 1 ⊢ inj f X Y, bij_is_inj 1.
04. 2 ⊢ inj g Y Z, bij_is_inj 2.
05. 1 ⊢ sur f X Y, bij_is_sur 1.
06. 2 ⊢ sur g Y Z, bij_is_sur 2.
07. 1, 2 ⊢ inj (g ∘ f) X Z, composition_inj_inj_is_inj 3 4.
08. 1, 2 ⊢ sur (g ∘ f) X Z, composition_sur_sur_is_sur 5 6.
09. 1, 2 ⊢ bij (g ∘ f) X Z, bij_from_inj_sur 7 8.
composition_bij_bij_is_bij. ⊢ bij f X Y → bij g Y Z →
  bij (g ∘ f) X Z, subj_intro_ii 9.

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