Theorem rng_composition

Proof
01. 1 ⊢ z ∈ rng (S ∘ R), hypo.
02. 1 ⊢ ∃x. (x, z) ∈ S ∘ R, rng_elim 1.
03. 3 ⊢ (x, z) ∈ S ∘ R, hypo.
04. 3 ⊢ ∃y. (y, z) ∈ S, composition_eliml 3.
05. 5 ⊢ (y, z) ∈ S, hypo.
06. 5 ⊢ z ∈ rng S, rng_intro 5.
07. 3 ⊢ z ∈ rng S, ex_elim 4 6.
08. 1 ⊢ z ∈ rng S, ex_elim 2 7.
09. ⊢ z ∈ rng (S ∘ R) → z ∈ rng S, subj_intro 8.
10. ⊢ ∀z. z ∈ rng (S ∘ R) → z ∈ rng S, uq_intro 9.
rng_composition. ⊢ rng (S ∘ R) ⊆ rng S, incl_intro 10.

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