We will prove connected_space (product_space ω (const_space_family ω R R_standard_topology)) (product_topology_full ω (const_space_family ω R R_standard_topology)).
Set Xi to be the term const_space_family ω R R_standard_topology.
Set X to be the term product_space ω Xi.
Set Tx to be the term product_topology_full ω Xi.
Set A to be the term Romega_infty.
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 HAsub: A ⊆ X.
An exact proof term for the current goal is Romega_infty_sub_Romega.
We prove the intermediate claim HAconn: connected_space A (subspace_topology X Tx A).
An exact proof term for the current goal is Romega_infty_connected.
We prove the intermediate claim Hdense: closure_of X Tx A = X.
An exact proof term for the current goal is Romega_infty_dense.
An exact proof term for the current goal is (connected_space_if_dense_connected_subset X Tx A HTx HAsub HAconn Hdense).
∎