Let X, Y, Z, f and g be given.
Assume Hf: function_on f X Y.
Assume Hg: function_on g Y Z.
We prove the intermediate claim Hsub: compose_fun X f g ⊆ setprod X Z.
Let p be given.
Assume Hp: p ∈ compose_fun X f g.
We will prove p ∈ setprod X Z.
Apply (ReplE_impred X (λx0 : set ⇒ (x0,apply_fun g (apply_fun f x0))) p Hp (p ∈ setprod X Z)) to the current goal.
Let x be given.
Assume HxX: x ∈ X.
Assume Heq: p = (x,apply_fun g (apply_fun f x)).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf x HxX).
We prove the intermediate claim HgxZ: apply_fun g (apply_fun f x) ∈ Z.
An exact proof term for the current goal is (Hg (apply_fun f x) HfxY).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X Z x (apply_fun g (apply_fun f x)) HxX HgxZ).
We prove the intermediate claim Hpow: compose_fun X f g ∈ 𝒫 (setprod X Z).
An exact proof term for the current goal is (PowerI (setprod X Z) (compose_fun X f g) Hsub).
We prove the intermediate claim Hfun: function_on (compose_fun X f g) X Z.
An exact proof term for the current goal is (function_on_compose_fun X Y Z f g Hf Hg).
An exact proof term for the current goal is (SepI (𝒫 (setprod X Z)) (λh0 : set ⇒ function_on h0 X Z) (compose_fun X f g) Hpow Hfun).
∎