We will prove connected_space Romega_infty (subspace_topology R_omega_space R_omega_product_topology Romega_infty).
Set X to be the term R_omega_space.
Set Tx to be the term R_omega_product_topology.
Set F to be the term {Romega_tilde n|n ∈ ω}.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is Romega_product_topology_is_topology.
We prove the intermediate claim HFsub: ∀C : set, C ∈ F → C ⊆ X.
Let C be given.
Assume HC: C ∈ F.
We will prove C ⊆ X.
Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) C HC (C ⊆ X)) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume HCeq: C = Romega_tilde n.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (Romega_tilde_sub_Romega n).
We prove the intermediate claim HFconn: ∀C : set, C ∈ F → connected_space C (subspace_topology X Tx C).
Let C be given.
Assume HC: C ∈ F.
We will prove connected_space C (subspace_topology X Tx C).
Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) C HC (connected_space C (subspace_topology X Tx C))) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume HCeq: C = Romega_tilde n.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (Romega_tilde_connected n Hn).
We prove the intermediate claim Hcommon: ∃x : set, ∀C : set, C ∈ F → x ∈ C.
We use Romega_zero to witness the existential quantifier.
Let C be given.
Assume HC: C ∈ F.
We will prove Romega_zero ∈ C.
Apply (ReplE_impred ω (λn : set ⇒ Romega_tilde n) C HC (Romega_zero ∈ C)) to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume HCeq: C = Romega_tilde n.
rewrite the current goal using HCeq (from left to right).
An exact proof term for the current goal is (Romega_zero_in_Romega_tilde n Hn).
We prove the intermediate claim HconnUnion: connected_space (⋃ F) (subspace_topology X Tx (⋃ F)).
An exact proof term for the current goal is (union_connected_common_point X Tx F HTx HFsub HFconn Hcommon).
We prove the intermediate claim HUnionEq: ⋃ F = Romega_infty.
Use reflexivity.
rewrite the current goal using HUnionEq (from left to right).
rewrite the current goal using HUnionEq (from left to right) at position 1.
An exact proof term for the current goal is HconnUnion.
∎