Let k and f be given.

Assume HkO: k ∈ ω.

Assume Hf: f ∈ R_omega_space.

We will prove apply_fun (Romega_restrict_map k) f = Romega_restrict_seq k f.

We prove the intermediate claim Hdef: Romega_restrict_map k = graph R_omega_space (λg : set ⇒ Romega_restrict_seq k g).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

An exact proof term for the current goal is (apply_fun_graph R_omega_space (λg : set ⇒ Romega_restrict_seq k g) f Hf).

∎