Let k be given.
Assume HkO: k ∈ ω.
Let f be given.
Assume Hf: f ∈ image_of (Romega_extend_map k) (setprod (Romega_tilde k) R).
We will prove f ∈ Romega_tilde (ordsucc k).
Apply (ReplE_impred (setprod (Romega_tilde k) R) (λp0 : set ⇒ apply_fun (Romega_extend_map k) p0) f Hf (f ∈ Romega_tilde (ordsucc k))) to the current goal.
Let p be given.
Assume Hp: p ∈ setprod (Romega_tilde k) R.
Assume Hfeq: f = apply_fun (Romega_extend_map k) p.
rewrite the current goal using Hfeq (from left to right).
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).
∎