Let p be given.
Assume Hp: p ∈ setprod R_omega_space R_omega_space.
We will prove apply_fun Romega_D_metric p ∈ R.
We prove the intermediate claim Happ: apply_fun Romega_D_metric p = Romega_D_metric_value (p 0) (p 1).
An exact proof term for the current goal is (apply_fun_graph (setprod R_omega_space R_omega_space) (λq : set ⇒ Romega_D_metric_value (q 0) (q 1)) p Hp).
rewrite the current goal using Happ (from left to right).
We prove the intermediate claim Hp0: p 0 ∈ R_omega_space.
An exact proof term for the current goal is (ap0_Sigma R_omega_space (λ_ : set ⇒ R_omega_space) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ R_omega_space.
An exact proof term for the current goal is (ap1_Sigma R_omega_space (λ_ : set ⇒ R_omega_space) p Hp).
An exact proof term for the current goal is (Romega_D_metric_value_in_R (p 0) (p 1) Hp0 Hp1).
∎