Theorem img_composition

Proof
01. 1 ⊢ z ∈ img (S ∘ R) A, hypo.
02. 1 ⊢ ∃x. x ∈ A ∧ (x, z) ∈ S ∘ R, img_elim 1.
03. 3 ⊢ x ∈ A ∧ (x, z) ∈ S ∘ R, hypo.
04. 3 ⊢ x ∈ A, conj_eliml 3.
05. 3 ⊢ (x, z) ∈ S ∘ R, conj_elimr 3.
06. 3 ⊢ ∃y. (x, y) ∈ R ∧ (y, z) ∈ S, composition_elim 5.
07. 7 ⊢ (x, y) ∈ R ∧ (y, z) ∈ S, hypo.
08. 7 ⊢ (x, y) ∈ R, conj_eliml 7.
09. 3, 7 ⊢ y ∈ img R A, img_intro 4 8.
10. 7 ⊢ (y, z) ∈ S, conj_elimr 7.
11. 3, 7 ⊢ z ∈ img S (img R A), img_intro 9 10.
12. 3 ⊢ z ∈ img S (img R A), ex_elim 6 11.
13. 1 ⊢ z ∈ img S (img R A), ex_elim 2 12.
14. ⊢ z ∈ img (S ∘ R) A → z ∈ img S (img R A), subj_intro 13.
15. 15 ⊢ z ∈ img S (img R A), hypo.
16. 15 ⊢ ∃y. y ∈ img R A ∧ (y, z) ∈ S, img_elim 15.
17. 17 ⊢ y ∈ img R A ∧ (y, z) ∈ S, hypo.
18. 17 ⊢ y ∈ img R A, conj_eliml 17.
19. 17 ⊢ ∃x. x ∈ A ∧ (x, y) ∈ R, img_elim 18.
20. 20 ⊢ x ∈ A ∧ (x, y) ∈ R, hypo.
21. 20 ⊢ x ∈ A, conj_eliml 20.
22. 20 ⊢ (x, y) ∈ R, conj_elimr 20.
23. 17 ⊢ (y, z) ∈ S, conj_elimr 17.
24. 17, 20 ⊢ (x, z) ∈ S ∘ R, composition_intro 22 23.
25. 17, 20 ⊢ z ∈ img (S ∘ R) A, img_intro 21 24.
26. 17 ⊢ z ∈ img (S ∘ R) A, ex_elim 19 25.
27. 15 ⊢ z ∈ img (S ∘ R) A, ex_elim 16 26.
28. ⊢ z ∈ img S (img R A) → z ∈ img (S ∘ R) A, subj_intro 27.
29. ⊢ z ∈ img (S ∘ R) A ↔ z ∈ img S (img R A), bij_intro 14 28.
30. ⊢ ∀z. z ∈ img (S ∘ R) A ↔ z ∈ img S (img R A), uq_intro 29.
img_composition. ⊢ img (S ∘ R) A = img S (img R A), ext 30.

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