Let f and i be given.
Assume Hf: f ∈ R_omega_space.
Assume Hi: i ∈ ω.
We will prove apply_fun f i ∈ R.
Set Xi to be the term const_space_family ω R R_standard_topology.
We prove the intermediate claim Hfprop: total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f ∧ ∀j : set, j ∈ ω → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω (space_family_union ω Xi))) (λf0 : set ⇒ total_function_on f0 ω (space_family_union ω Xi) ∧ functional_graph f0 ∧ ∀j : set, j ∈ ω → apply_fun f0 j ∈ space_family_set Xi j) f Hf).
We prove the intermediate claim Hcoords: ∀j : set, j ∈ ω → apply_fun f j ∈ space_family_set Xi j.
An exact proof term for the current goal is (andER (total_function_on f ω (space_family_union ω Xi) ∧ functional_graph f) (∀j : set, j ∈ ω → apply_fun f j ∈ space_family_set Xi j) Hfprop).
We prove the intermediate claim Hfi: apply_fun f i ∈ space_family_set Xi i.
An exact proof term for the current goal is (Hcoords i Hi).
We prove the intermediate claim HXi: apply_fun Xi i = (R,R_standard_topology).
An exact proof term for the current goal is (const_space_family_apply ω R R_standard_topology i Hi).
We prove the intermediate claim Hset: space_family_set Xi i = R.
We prove the intermediate claim Hdef: space_family_set Xi i = (apply_fun Xi i) 0.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using HXi (from left to right).
An exact proof term for the current goal is (tuple_2_0_eq R R_standard_topology).
rewrite the current goal using Hset (from right to left).
An exact proof term for the current goal is Hfi.
∎