Let k and f be given.
Assume HkO: k ∈ ω.
Assume Hf: f ∈ R_omega_space.
We will prove Romega_restrict_seq k f ∈ Romega_tilde k.
Set h to be the term (λi : set ⇒ If_i (k ∈ i) 0 (apply_fun f i)).
We prove the intermediate claim Hdef: Romega_restrict_seq k f = graph ω h.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
We prove the intermediate claim HdefT: Romega_tilde k = {g ∈ R_omega_space|∀i : set, i ∈ ω → k ∈ i → apply_fun g i = 0}.
Use reflexivity.
rewrite the current goal using HdefT (from left to right).
Apply (SepI R_omega_space (λg0 : set ⇒ ∀i : set, i ∈ ω → k ∈ i → apply_fun g0 i = 0)) to the current goal.
Apply (graph_omega_in_Romega_space h) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
We will prove h i ∈ R.
We prove the intermediate claim Hhi: h i = If_i (k ∈ i) 0 (apply_fun f i).
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
Apply (xm (k ∈ i)) to the current goal.
Assume Hki: k ∈ i.
rewrite the current goal using (If_i_1 (k ∈ i) 0 (apply_fun f i) Hki) (from left to right).
An exact proof term for the current goal is real_0.
Assume Hnki: ¬ (k ∈ i).
rewrite the current goal using (If_i_0 (k ∈ i) 0 (apply_fun f i) Hnki) (from left to right).
An exact proof term for the current goal is (Romega_coord_in_R f i Hf Hi).
Let i be given.
Assume Hi: i ∈ ω.
Assume Hki: k ∈ i.
We will prove apply_fun (graph ω h) i = 0.
We prove the intermediate claim Happ: apply_fun (graph ω h) i = h i.
An exact proof term for the current goal is (apply_fun_graph ω h i Hi).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hhi: h i = If_i (k ∈ i) 0 (apply_fun f i).
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
rewrite the current goal using (If_i_1 (k ∈ i) 0 (apply_fun f i) Hki) (from left to right).
Use reflexivity.
∎