Let k and f be given.
Assume HkO: k ∈ ω.
Assume Hf: f ∈ Romega_tilde (ordsucc k).
We will prove apply_fun (Romega_split_map k) f = (Romega_restrict_seq k f,apply_fun f (ordsucc k)).
We prove the intermediate claim Hdef: Romega_split_map k = graph (Romega_tilde (ordsucc k)) (λg : set ⇒ (Romega_restrict_seq k g,apply_fun g (ordsucc k))).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (apply_fun_graph (Romega_tilde (ordsucc k)) (λg : set ⇒ (Romega_restrict_seq k g,apply_fun g (ordsucc k))) f Hf).
∎