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