Let n and f be given.
Assume Hf: f ∈ euclidean_space n.
Set h to be the term (λi : set ⇒ If_i (i ∈ n) (apply_fun f i) 0).
We prove the intermediate claim Hdef: euclidean_space_extend_to_Romega n f = graph ω h.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (graph_omega_in_Romega_space h) to the current goal.
Let i be given.
Assume Hi: i ∈ ω.
Apply xm (i ∈ n) to the current goal.
Assume Hin: i ∈ n.
We prove the intermediate claim HfiR: apply_fun f i ∈ R.
An exact proof term for the current goal is (euclidean_space_coord_in_R n f i Hf Hin).
We prove the intermediate claim Hhi: h i = If_i (i ∈ n) (apply_fun f i) 0.
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
rewrite the current goal using (If_i_1 (i ∈ n) (apply_fun f i) 0 Hin) (from left to right).
An exact proof term for the current goal is HfiR.
Assume Hnin: ¬ (i ∈ n).
We prove the intermediate claim Hhi: h i = If_i (i ∈ n) (apply_fun f i) 0.
Use reflexivity.
rewrite the current goal using Hhi (from left to right).
rewrite the current goal using (If_i_0 (i ∈ n) (apply_fun f i) 0 Hnin) (from left to right).
An exact proof term for the current goal is real_0.
∎