Let k be given.
Assume HkO: k ∈ ω.
We will prove function_on (Romega_split_map k) (Romega_tilde (ordsucc k)) (setprod (Romega_tilde k) R).
Let f be given.
Assume Hf: f ∈ Romega_tilde (ordsucc k).
We will prove apply_fun (Romega_split_map k) f ∈ setprod (Romega_tilde k) R.
rewrite the current goal using (Romega_split_map_apply k f HkO Hf) (from left to right).
We prove the intermediate claim HfRomega: f ∈ R_omega_space.
An exact proof term for the current goal is (Romega_tilde_sub_Romega (ordsucc k) f Hf).
We prove the intermediate claim Hkf: 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 HfRomega).
We prove the intermediate claim HsuccO: ordsucc k ∈ ω.
An exact proof term for the current goal is (omega_ordsucc k HkO).
We prove the intermediate claim Hfcoord: apply_fun f (ordsucc k) ∈ R.
An exact proof term for the current goal is (Romega_coord_in_R f (ordsucc k) HfRomega HsuccO).
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma (Romega_tilde k) R (Romega_restrict_seq k f) (apply_fun f (ordsucc k)) Hkf Hfcoord).
∎