Let X, Y, Z, f and g be given.
Assume Hf: function_on f X Y.
Assume Hg: function_on g Y Z.
Let x be given.
Assume HxX: x ∈ X.
We will prove apply_fun (compose_fun X f g) x ∈ Z.
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 HgfxZ: apply_fun g (apply_fun f x) ∈ Z.
An exact proof term for the current goal is (Hg (apply_fun f x) HfxY).
We prove the intermediate claim Hpair: (x,apply_fun g (apply_fun f x)) ∈ compose_fun X f g.
An exact proof term for the current goal is (ReplI X (λx0 : set ⇒ (x0,apply_fun g (apply_fun f x0))) x HxX).
We prove the intermediate claim Hfuncomp: functional_graph (compose_fun X f g).
An exact proof term for the current goal is (functional_graph_compose_fun X f g).
We prove the intermediate claim Happ: apply_fun (compose_fun X f g) x = apply_fun g (apply_fun f x).
An exact proof term for the current goal is (functional_graph_apply_fun_eq (compose_fun X f g) x (apply_fun g (apply_fun f x)) Hfuncomp Hpair).
rewrite the current goal using Happ (from left to right).
An exact proof term for the current goal is HgfxZ.
∎