Let k be given.
Assume HkO: k ∈ ω.
We will prove function_on (Romega_extend_map k) (setprod (Romega_tilde k) R) R_omega_space.
Let p be given.
Assume Hp: p ∈ setprod (Romega_tilde k) R.
We will prove apply_fun (Romega_extend_map k) p ∈ R_omega_space.
rewrite the current goal using (Romega_extend_map_apply k p HkO Hp) (from left to right).
We prove the intermediate claim Htilde: Romega_extend_seq k p ∈ Romega_tilde (ordsucc k).
An exact proof term for the current goal is (Romega_extend_seq_in_Romega_tilde_succ k p HkO Hp).
An exact proof term for the current goal is (Romega_tilde_sub_Romega (ordsucc k) (Romega_extend_seq k p) Htilde).
∎