Let k, f and i be given.
Assume HkO: k ∈ ω.
Assume Hf: f ∈ R_omega_space.
Assume Hi: i ∈ ω.
We will prove apply_fun (Romega_restrict_seq k f) i = If_i (k ∈ i) 0 (apply_fun f i).
We prove the intermediate claim Hdef: Romega_restrict_seq k f = graph ω (λj : set ⇒ If_i (k ∈ j) 0 (apply_fun f j)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph ω (λj : set ⇒ If_i (k ∈ j) 0 (apply_fun f j)) i Hi).
∎