Let Xi, Ti, i, a, b and f be given.
Assume Hchain: coherent_chain Xi Ti.
Assume HiO: i ∈ ω.
Assume Hab: Rle a b.
Assume HnormS: normal_space (apply_fun Xi (ordsucc i)) (apply_fun Ti (ordsucc i)).
Assume Hf: continuous_map (apply_fun Xi i) (apply_fun Ti i) (closed_interval a b) (closed_interval_topology a b) f.
Set Xi_i to be the term apply_fun Xi i.
Set Ti_i to be the term apply_fun Ti i.
Set Xi_s to be the term apply_fun Xi (ordsucc i).
Set Ti_s to be the term apply_fun Ti (ordsucc i).
Set A0 to be the term (∀j : set, j ∈ ω → topology_on (apply_fun Xi j) (apply_fun Ti j)).
Set B0 to be the term (∀j : set, j ∈ ω → apply_fun Xi j ⊆ apply_fun Xi (ordsucc j)).
Set C0 to be the term (∀j : set, j ∈ ω → subspace_topology (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j) = apply_fun Ti j).
Set D0 to be the term (∀j : set, j ∈ ω → closed_in (apply_fun Xi (ordsucc j)) (apply_fun Ti (ordsucc j)) (apply_fun Xi j)).
We prove the intermediate claim Habc: (A0 ∧ B0) ∧ C0.
An exact proof term for the current goal is (andEL ((A0 ∧ B0) ∧ C0) D0 Hchain).
We prove the intermediate claim HD: D0.
An exact proof term for the current goal is (andER ((A0 ∧ B0) ∧ C0) D0 Hchain).
We prove the intermediate claim HC: C0.
An exact proof term for the current goal is (andER (A0 ∧ B0) C0 Habc).
We prove the intermediate claim Hsubeq: subspace_topology Xi_s Ti_s Xi_i = Ti_i.
An exact proof term for the current goal is (HC i HiO).
We prove the intermediate claim HXi_i_closed: closed_in Xi_s Ti_s Xi_i.
An exact proof term for the current goal is (HD i HiO).
We prove the intermediate claim Hfsub: continuous_map Xi_i (subspace_topology Xi_s Ti_s Xi_i) (closed_interval a b) (closed_interval_topology a b) f.
rewrite the current goal using Hsubeq (from left to right).
An exact proof term for the current goal is Hf.
An exact proof term for the current goal is (Tietze_extension_interval Xi_s Ti_s Xi_i a b f Hab HnormS HXi_i_closed Hfsub).
∎