Let f be given.
Assume Hf: f ∈ component_of (product_space ω (const_space_family ω R R_standard_topology)) (box_topology ω (const_space_family ω R R_standard_topology)) (const_family ω 0).
We will prove f ∈ Romega_infty.
Set X to be the term product_space ω (const_space_family ω R R_standard_topology).
Set Tx to be the term box_topology ω (const_space_family ω R R_standard_topology).
Set x0 to be the term const_family ω 0.
We prove the intermediate claim HfCpack: ∃C : set, connected_space C (subspace_topology X Tx C) ∧ x0 ∈ C ∧ f ∈ C.
An exact proof term for the current goal is (SepE2 X (λy : set ⇒ ∃C0 : set, connected_space C0 (subspace_topology X Tx C0) ∧ x0 ∈ C0 ∧ y ∈ C0) f Hf).
Apply HfCpack to the current goal.
Let C be given.
Assume HCpack.
We prove the intermediate claim HCcore: connected_space C (subspace_topology X Tx C) ∧ x0 ∈ C.
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology X Tx C) ∧ x0 ∈ C) (f ∈ C) HCpack).
We prove the intermediate claim Hf_in_C: f ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C) ∧ x0 ∈ C) (f ∈ C) HCpack).
We prove the intermediate claim HCconn: connected_space C (subspace_topology X Tx C).
An exact proof term for the current goal is (andEL (connected_space C (subspace_topology X Tx C)) (x0 ∈ C) HCcore).
We prove the intermediate claim Hx0C: x0 ∈ C.
An exact proof term for the current goal is (andER (connected_space C (subspace_topology X Tx C)) (x0 ∈ C) HCcore).
The rest of this subproof is missing.
∎