Let i and U be given.
Assume HiO: i ∈ ω.
Assume HUtop: U ∈ space_family_topology (const_space_family ω R R_standard_topology) i.
Set Xi to be the term const_space_family ω R R_standard_topology.
Set X to be the term product_space ω Xi.
Set S to be the term product_subbasis_full ω Xi.
Set Cyl to be the term product_cylinder ω Xi i U.
We prove the intermediate claim HS: subbasis_on R_omega_space S.
An exact proof term for the current goal is Romega_product_subbasis_on.
We prove the intermediate claim HSin: Cyl ∈ S.
Set F to be the term (λj : set ⇒ {product_cylinder ω Xi j V|V ∈ space_family_topology Xi j}).
We prove the intermediate claim HCylFi: Cyl ∈ F i.
An exact proof term for the current goal is (ReplI (space_family_topology Xi i) (λV : set ⇒ product_cylinder ω Xi i V) U HUtop).
An exact proof term for the current goal is (famunionI ω F i Cyl HiO HCylFi).
We prove the intermediate claim HdefT: R_omega_product_topology = generated_topology_from_subbasis R_omega_space S.
Use reflexivity.
rewrite the current goal using HdefT (from left to right).
An exact proof term for the current goal is (subbasis_elem_open_in_generated_from_subbasis R_omega_space S Cyl HS HSin).
∎