Let i be given.

Assume Hi: i ∈ ω.

We will prove function_on (Romega_coord_map i) R_omega_space R.

Let f be given.

Assume Hf: f ∈ R_omega_space.

We will prove apply_fun (Romega_coord_map i) f ∈ R.

rewrite the current goal using (Romega_coord_map_apply i f Hi Hf) (from left to right).

An exact proof term for the current goal is (Romega_coord_in_R f i Hf Hi).

∎