Let g be given.
Assume Hg: ∀i : set, i ∈ ω → g i ∈ R.
Set Xi to be the term const_space_family ω R R_standard_topology.
We will prove graph ω g ∈ product_space ω Xi.
We prove the intermediate claim Hdef: product_space ω Xi = {f ∈ 𝒫 (setprod ω (space_family_union ω Xi))|total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀i0 : set, i0 ∈ ω → apply_fun f i0 ∈ space_family_set Xi i0}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply SepI to the current goal.
We prove the intermediate claim HUnion: space_family_union ω Xi = R.
An exact proof term for the current goal is space_family_union_const_Romega.
rewrite the current goal using HUnion (from left to right).
Apply (PowerI (setprod ω R) (graph ω g)) to the current goal.
Let p be given.
Assume Hp: p ∈ graph ω g.
We will prove p ∈ setprod ω R.
Apply (ReplE_impred ω (λi0 : set ⇒ (i0,g i0)) p Hp (p ∈ setprod ω R)) to the current goal.
Let i be given.
Assume HiO: i ∈ ω.
Assume Hpeq: p = (i,g i).
rewrite the current goal using Hpeq (from left to right).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma ω R i (g i) HiO (Hg i HiO)).
We will prove total_function_on (graph ω g) ω (space_family_union ω Xi) ∧ functional_graph (graph ω g) ∧ ∀i0 : set, i0 ∈ ω → apply_fun (graph ω g) i0 ∈ space_family_set Xi i0.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HUnion2: space_family_union ω Xi = R.
An exact proof term for the current goal is space_family_union_const_Romega.
rewrite the current goal using HUnion2 (from left to right).
An exact proof term for the current goal is (total_function_on_graph ω R g Hg).
An exact proof term for the current goal is (functional_graph_graph ω g).
Let i be given.
Assume HiO: i ∈ ω.
We will prove apply_fun (graph ω g) i ∈ space_family_set Xi i.
rewrite the current goal using (space_family_set_const_Romega i HiO) (from left to right).
rewrite the current goal using (apply_fun_graph ω g i HiO) (from left to right).
An exact proof term for the current goal is (Hg i HiO).
∎