Let n be given.

Assume Hn: n ∈ ω.

We will prove connected_space (Romega_tilde n) (subspace_topology R_omega_space R_omega_box_topology (Romega_tilde n)).

We prove the intermediate claim Heq: subspace_topology R_omega_space R_omega_box_topology (Romega_tilde n) = subspace_topology R_omega_space R_omega_product_topology (Romega_tilde n).

An exact proof term for the current goal is (Romega_tilde_subspace_box_eq_product n Hn).

rewrite the current goal using Heq (from left to right).

An exact proof term for the current goal is (Romega_tilde_connected n Hn).

∎