Let X, Y, Z, f and g be given.
Assume Hf: function_on f X Y.
Assume Hg: function_on g Y Z.
We will prove function_on (compose_fun X f g) X Z ∧ ∀x : set, x ∈ X → ∃y : set, y ∈ Z ∧ (x,y) ∈ compose_fun X f g.
Apply andI to the current goal.
An exact proof term for the current goal is (function_on_compose_fun X Y Z f g Hf Hg).
Let x be given.
Assume HxX: x ∈ X.
We will prove ∃y : set, y ∈ Z ∧ (x,y) ∈ compose_fun X f g.
We use (apply_fun g (apply_fun f x)) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HfxY: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hf x HxX).
An exact proof term for the current goal is (Hg (apply_fun f x) HfxY).
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ (x0,apply_fun g (apply_fun f x0))) x HxX).
∎