We prove the intermediate claim Hrules: (∀y0 : set, y0 ∈ Y → continuous_map X Tx Y Ty (const_fun X y0)) ∧ (∀A : set, A ⊆ X → continuous_map A (subspace_topology X Tx A) X Tx {(y,y)|y ∈ A}) ∧ (∀f0 g0 : set, continuous_map X Tx Y Ty f0 → continuous_map Y Ty Y Ty g0 → continuous_map X Tx Y Ty (compose_fun X f0 g0)) ∧ (∀f0 A : set, A ⊆ X → continuous_map X Tx Y Ty f0 → continuous_map A (subspace_topology X Tx A) Y Ty f0) ∧ ((∀f0 Z0 : set, continuous_map X Tx Y Ty f0 → Z0 ⊆ Y → (∀x : set, x ∈ X → apply_fun f0 x ∈ Z0) → continuous_map X Tx Z0 (subspace_topology Y Ty Z0) f0) ∧ (∀f0 Z0 Tz0 : set, continuous_map X Tx Y Ty f0 → Y ⊆ Z0 → topology_on Z0 Tz0 → Ty = subspace_topology Z0 Tz0 Y → continuous_map X Tx Z0 Tz0 f0)) ∧ (∀f0 : set, (∃UFam : set, UFam ⊆ Tx ∧ ⋃ UFam = X ∧ (∀U : set, U ∈ UFam → continuous_map U (subspace_topology X Tx U) Y Ty f0)) → continuous_map X Tx Y Ty f0).

Apply (and6E (∀y0 : set, y0 ∈ Y → continuous_map X Tx Y Ty (const_fun X y0)) (∀A : set, A ⊆ X → continuous_map A (subspace_topology X Tx A) X Tx {(y,y)|y ∈ A}) (∀f0 g0 : set, continuous_map X Tx Y Ty f0 → continuous_map Y Ty Y Ty g0 → continuous_map X Tx Y Ty (compose_fun X f0 g0)) (∀f0 A : set, A ⊆ X → continuous_map X Tx Y Ty f0 → continuous_map A (subspace_topology X Tx A) Y Ty f0) ((∀f0 Z0 : set, continuous_map X Tx Y Ty f0 → Z0 ⊆ Y → (∀x : set, x ∈ X → apply_fun f0 x ∈ Z0) → continuous_map X Tx Z0 (subspace_topology Y Ty Z0) f0) ∧ (∀f0 Z0 Tz0 : set, continuous_map X Tx Y Ty f0 → Y ⊆ Z0 → topology_on Z0 Tz0 → Ty = subspace_topology Z0 Tz0 Y → continuous_map X Tx Z0 Tz0 f0)) (∀f0 : set, (∃UFam : set, UFam ⊆ Tx ∧ ⋃ UFam = X ∧ (∀U : set, U ∈ UFam → continuous_map U (subspace_topology X Tx U) Y Ty f0)) → continuous_map X Tx Y Ty f0) Hrules (continuous_map X Tx Y Ty f)) to the current goal.