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