Let X, Tx, Y, Ty, Z, Tz, f and g be given.
Assume Hf: continuous_map X Tx Y Ty f.
Assume Hg: continuous_map Y Ty Z Tz g.
We will prove continuous_map X Tx Z Tz (compose_fun X f g).
Set gf to be the term compose_fun X f g.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (topology_on Y Ty) (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) (andEL (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf))).
We prove the intermediate claim HTy_from_f: topology_on Y Ty.
An exact proof term for the current goal is (andER (topology_on X Tx) (topology_on Y Ty) (andEL (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) (andEL (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf))).
We prove the intermediate claim Hfun_f: function_on f X Y.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty) (function_on f X Y) (andEL (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf)).
We prove the intermediate claim Hpreimg_f: ∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ topology_on Y Ty ∧ function_on f X Y) (∀V : set, V ∈ Ty → preimage_of X f V ∈ Tx) Hf).
We prove the intermediate claim HTy: topology_on Y Ty.
An exact proof term for the current goal is (andEL (topology_on Y Ty) (topology_on Z Tz) (andEL (topology_on Y Ty ∧ topology_on Z Tz) (function_on g Y Z) (andEL (topology_on Y Ty ∧ topology_on Z Tz ∧ function_on g Y Z) (∀W : set, W ∈ Tz → preimage_of Y g W ∈ Ty) Hg))).
We prove the intermediate claim HTz: topology_on Z Tz.
An exact proof term for the current goal is (andER (topology_on Y Ty) (topology_on Z Tz) (andEL (topology_on Y Ty ∧ topology_on Z Tz) (function_on g Y Z) (andEL (topology_on Y Ty ∧ topology_on Z Tz ∧ function_on g Y Z) (∀W : set, W ∈ Tz → preimage_of Y g W ∈ Ty) Hg))).
We prove the intermediate claim Hfun_g: function_on g Y Z.
An exact proof term for the current goal is (andER (topology_on Y Ty ∧ topology_on Z Tz) (function_on g Y Z) (andEL (topology_on Y Ty ∧ topology_on Z Tz ∧ function_on g Y Z) (∀W : set, W ∈ Tz → preimage_of Y g W ∈ Ty) Hg)).
We prove the intermediate claim Hpreimg_g: ∀W : set, W ∈ Tz → preimage_of Y g W ∈ Ty.
An exact proof term for the current goal is (andER (topology_on Y Ty ∧ topology_on Z Tz ∧ function_on g Y Z) (∀W : set, W ∈ Tz → preimage_of Y g W ∈ Ty) Hg).
We will prove topology_on X Tx ∧ topology_on Z Tz ∧ function_on gf X Z ∧ (∀W : set, W ∈ Tz → preimage_of X gf W ∈ Tx).
We prove the intermediate claim Hpart1: topology_on X Tx ∧ topology_on Z Tz.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HTz.
We prove the intermediate claim Hpart2: (topology_on X Tx ∧ topology_on Z Tz) ∧ function_on gf X Z.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart1.
We will prove ∀x : set, x ∈ X → apply_fun gf x ∈ Z.
Let x be given.
Assume Hx: x ∈ X.
We will prove apply_fun gf x ∈ Z.
We prove the intermediate claim Hfx: apply_fun f x ∈ Y.
An exact proof term for the current goal is (Hfun_f x Hx).
We prove the intermediate claim Hgfx: apply_fun g (apply_fun f x) ∈ Z.
An exact proof term for the current goal is (Hfun_g (apply_fun f x) Hfx).
We prove the intermediate claim Hgf_eq: apply_fun gf x = apply_fun g (apply_fun f x).
An exact proof term for the current goal is (compose_fun_apply X f g x Hx).
rewrite the current goal using Hgf_eq (from left to right).
An exact proof term for the current goal is Hgfx.
Apply andI to the current goal.
An exact proof term for the current goal is Hpart2.
Let W be given.
Assume HW: W ∈ Tz.
We will prove preimage_of X gf W ∈ Tx.
We prove the intermediate claim HgW_open: preimage_of Y g W ∈ Ty.
An exact proof term for the current goal is (Hpreimg_g W HW).
We prove the intermediate claim HfgW_open: preimage_of X f (preimage_of Y g W) ∈ Tx.
An exact proof term for the current goal is (Hpreimg_f (preimage_of Y g W) HgW_open).
We prove the intermediate claim Hpreimg_eq: preimage_of X gf W = preimage_of X f (preimage_of Y g W).
An exact proof term for the current goal is (preimage_compose_fun X Y f g W Hfun_f).
rewrite the current goal using Hpreimg_eq (from left to right).
An exact proof term for the current goal is HfgW_open.
∎