Let k be given.
Assume HkO: k ∈ ω.
We will prove function_on (Romega_restrict_map k) R_omega_space R_omega_space.
Let f be given.
Assume Hf: f ∈ R_omega_space.
We will prove apply_fun (Romega_restrict_map k) f ∈ R_omega_space.
rewrite the current goal using (Romega_restrict_map_apply k f HkO Hf) (from left to right).
We prove the intermediate claim Htilde: Romega_restrict_seq k f ∈ Romega_tilde k.
An exact proof term for the current goal is (Romega_restrict_seq_in_Romega_tilde k f HkO Hf).
An exact proof term for the current goal is (Romega_tilde_sub_Romega k (Romega_restrict_seq k f) Htilde).
∎