Let s be given.

Assume Hs: s ∈ S.

We will prove s ∈ 𝒫 R_omega_space.

Apply PowerI to the current goal.

Let f be given.

Assume Hf: f ∈ s.

We will prove f ∈ R_omega_space.

Set F to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).

We prove the intermediate claim HsF: s ∈ (⋃_{i ∈ ω}F i).

An exact proof term for the current goal is Hs.

Apply (famunionE_impred ω F s HsF (f ∈ R_omega_space)) to the current goal.

Let i be given.

Assume Hi: i ∈ ω.

Assume HsFi: s ∈ F i.

Apply (ReplE_impred (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) s HsFi (f ∈ R_omega_space)) to the current goal.

Let U be given.

Assume HUtop: U ∈ space_family_topology Xi i.

Assume Hseq: s = product_cylinder ω Xi i U.

We prove the intermediate claim HfCyl: f ∈ product_cylinder ω Xi i U.

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

An exact proof term for the current goal is Hf.

We prove the intermediate claim Hfprod: f ∈ product_space ω Xi.

An exact proof term for the current goal is (SepE1 (product_space ω Xi) (λg : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f HfCyl).

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

An exact proof term for the current goal is Hfprod.

Apply set_ext to the current goal.

Let f be given.

Assume HfU: f ∈ ⋃ S.

We will prove f ∈ R_omega_space.

Apply (UnionE_impred S f HfU (f ∈ R_omega_space)) to the current goal.

Let s be given.

Assume Hfs: f ∈ s.

Assume Hs: s ∈ S.

Set F to be the term (λi : set ⇒ {product_cylinder ω Xi i U|U ∈ space_family_topology Xi i}).

We prove the intermediate claim HsF: s ∈ (⋃_{i ∈ ω}F i).

An exact proof term for the current goal is Hs.

Apply (famunionE_impred ω F s HsF (f ∈ R_omega_space)) to the current goal.

Let i be given.

Assume Hi: i ∈ ω.

Assume HsFi: s ∈ F i.

Apply (ReplE_impred (space_family_topology Xi i) (λU0 : set ⇒ product_cylinder ω Xi i U0) s HsFi (f ∈ R_omega_space)) to the current goal.

Let U be given.

Assume HUtop: U ∈ space_family_topology Xi i.

Assume Hseq: s = product_cylinder ω Xi i U.

We prove the intermediate claim HfCyl: f ∈ product_cylinder ω Xi i U.

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

An exact proof term for the current goal is Hfs.

We prove the intermediate claim Hfprod: f ∈ product_space ω Xi.

An exact proof term for the current goal is (SepE1 (product_space ω Xi) (λg : set ⇒ i ∈ ω ∧ U ∈ space_family_topology Xi i ∧ apply_fun g i ∈ U) f HfCyl).

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

An exact proof term for the current goal is Hfprod.

Let f be given.

Assume HfX: f ∈ R_omega_space.

We will prove f ∈ ⋃ S.

Set s0 to be the term product_cylinder ω Xi 0 R.

We prove the intermediate claim H0o: 0 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

We prove the intermediate claim HRin: R ∈ space_family_topology Xi 0.

We prove the intermediate claim HXi0: apply_fun Xi 0 = (R,R_standard_topology).

An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology 0 H0o).

We prove the intermediate claim Htop0: space_family_topology Xi 0 = R_standard_topology.

We prove the intermediate claim Hdef: space_family_topology Xi 0 = (apply_fun Xi 0) 1.

Use reflexivity.

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

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

An exact proof term for the current goal is (tuple_2_1_eq R R_standard_topology).

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

An exact proof term for the current goal is (topology_has_X R R_standard_topology R_standard_topology_is_topology_local).

We prove the intermediate claim Hf0R: apply_fun f 0 ∈ R.

An exact proof term for the current goal is (Romega_coord_in_R f 0 HfX H0o).

We prove the intermediate claim Hfprod: f ∈ product_space ω Xi.

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

An exact proof term for the current goal is HfX.

We prove the intermediate claim Hfs0: f ∈ s0.

We prove the intermediate claim Hcyl_def: s0 = {g ∈ product_space ω Xi|0 ∈ ω ∧ R ∈ space_family_topology Xi 0 ∧ apply_fun g 0 ∈ R}.

Use reflexivity.

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

Apply (SepI (product_space ω Xi) (λg : set ⇒ 0 ∈ ω ∧ R ∈ space_family_topology Xi 0 ∧ apply_fun g 0 ∈ R) f Hfprod) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is H0o.

An exact proof term for the current goal is HRin.

An exact proof term for the current goal is Hf0R.

We prove the intermediate claim Hs0In: s0 ∈ {product_cylinder ω Xi 0 U0|U0 ∈ space_family_topology Xi 0}.

An exact proof term for the current goal is (ReplI (space_family_topology Xi 0) (λU0 : set ⇒ product_cylinder ω Xi 0 U0) R HRin).

We prove the intermediate claim Hs0S: s0 ∈ S.

An exact proof term for the current goal is (famunionI ω (λj : set ⇒ {product_cylinder ω Xi j U0|U0 ∈ space_family_topology Xi j}) 0 s0 H0o Hs0In).

An exact proof term for the current goal is (UnionI S f s0 Hfs0 Hs0S).