Apply set_ext to the current goal.
Let f be given.
Assume Hf: f ∈ real_sequences.
We will prove f ∈ R_omega_space.
We prove the intermediate claim Hdef: R_omega_space = product_space ω (const_space_family ω R R_standard_topology).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
We will prove f ∈ product_space ω (const_space_family ω R R_standard_topology).
We prove the intermediate claim Hproddef: product_space ω (const_space_family ω R R_standard_topology) = {f0 ∈ 𝒫 (setprod ω (space_family_union ω (const_space_family ω R R_standard_topology)))|total_function_on f0 ω (space_family_union ω (const_space_family ω R R_standard_topology)) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set (const_space_family ω R R_standard_topology) i}.
Use reflexivity.
rewrite the current goal using Hproddef (from left to right).
Apply (SepI (𝒫 (setprod ω (space_family_union ω (const_space_family ω R R_standard_topology)))) (λf0 : set ⇒ total_function_on f0 ω (space_family_union ω (const_space_family ω R R_standard_topology)) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set (const_space_family ω R R_standard_topology) i) f) to the current goal.
We prove the intermediate claim HfPow: f ∈ 𝒫 (setprod ω R).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω R)) (λf0 : set ⇒ total_function_on f0 ω R ∧ functional_graph f0) f Hf).
rewrite the current goal using (space_family_union_const_Romega) (from left to right).
An exact proof term for the current goal is HfPow.
We prove the intermediate claim Hpack: total_function_on f ω R ∧ functional_graph f.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω R)) (λf0 : set ⇒ total_function_on f0 ω R ∧ functional_graph f0) f Hf).
We prove the intermediate claim Htot: total_function_on f ω R.
An exact proof term for the current goal is (andEL (total_function_on f ω R) (functional_graph f) Hpack).
We prove the intermediate claim Hfun: functional_graph f.
An exact proof term for the current goal is (andER (total_function_on f ω R) (functional_graph f) Hpack).
Apply andI to the current goal.
Apply andI to the current goal.
rewrite the current goal using (space_family_union_const_Romega) (from left to right).
An exact proof term for the current goal is Htot.
An exact proof term for the current goal is Hfun.
Let i be given.
Assume HiO: i ∈ ω.
rewrite the current goal using (space_family_set_const_Romega i HiO) (from left to right).
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y f ω R i Htot HiO).
Let f be given.
Assume Hf: f ∈ R_omega_space.
We will prove f ∈ real_sequences.
We prove the intermediate claim Hdef: R_omega_space = product_space ω (const_space_family ω R R_standard_topology).
Use reflexivity.
We prove the intermediate claim Hproddef: product_space ω (const_space_family ω R R_standard_topology) = {f0 ∈ 𝒫 (setprod ω (space_family_union ω (const_space_family ω R R_standard_topology)))|total_function_on f0 ω (space_family_union ω (const_space_family ω R R_standard_topology)) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set (const_space_family ω R R_standard_topology) i}.
Use reflexivity.
We prove the intermediate claim HfP: f ∈ {f0 ∈ 𝒫 (setprod ω (space_family_union ω (const_space_family ω R R_standard_topology)))|total_function_on f0 ω (space_family_union ω (const_space_family ω R R_standard_topology)) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set (const_space_family ω R R_standard_topology) i}.
rewrite the current goal using Hproddef (from right to left).
rewrite the current goal using Hdef (from right to left).
An exact proof term for the current goal is Hf.
We prove the intermediate claim HfPowU: f ∈ 𝒫 (setprod ω (space_family_union ω (const_space_family ω R R_standard_topology))).
An exact proof term for the current goal is (SepE1 (𝒫 (setprod ω (space_family_union ω (const_space_family ω R R_standard_topology)))) (λf0 : set ⇒ total_function_on f0 ω (space_family_union ω (const_space_family ω R R_standard_topology)) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set (const_space_family ω R R_standard_topology) i) f HfP).
We prove the intermediate claim HfPred: total_function_on f ω (space_family_union ω (const_space_family ω R R_standard_topology)) ∧ functional_graph f ∧ ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set (const_space_family ω R R_standard_topology) i.
An exact proof term for the current goal is (SepE2 (𝒫 (setprod ω (space_family_union ω (const_space_family ω R R_standard_topology)))) (λf0 : set ⇒ total_function_on f0 ω (space_family_union ω (const_space_family ω R R_standard_topology)) ∧ functional_graph f0 ∧ ∀i : set, i ∈ ω → apply_fun f0 i ∈ space_family_set (const_space_family ω R R_standard_topology) i) f HfP).
Set A to be the term total_function_on f ω (space_family_union ω (const_space_family ω R R_standard_topology)).
Set B to be the term functional_graph f.
Set C to be the term ∀i : set, i ∈ ω → apply_fun f i ∈ space_family_set (const_space_family ω R R_standard_topology) i.
We prove the intermediate claim Hab: A ∧ B.
An exact proof term for the current goal is (andEL (A ∧ B) C HfPred).
We prove the intermediate claim HtotU: A.
An exact proof term for the current goal is (andEL A B Hab).
We prove the intermediate claim Hfun: B.
An exact proof term for the current goal is (andER A B Hab).
Apply (SepI (𝒫 (setprod ω R)) (λf0 : set ⇒ total_function_on f0 ω R ∧ functional_graph f0) f) to the current goal.
rewrite the current goal using (space_family_union_const_Romega) (from right to left).
An exact proof term for the current goal is HfPowU.
Apply andI to the current goal.
rewrite the current goal using (space_family_union_const_Romega) (from right to left).
An exact proof term for the current goal is HtotU.
An exact proof term for the current goal is Hfun.
∎