Let p be given.
Assume Hp: p ∈ setprod real_sequences real_sequences.
We will prove apply_fun uniform_metric_Romega p ∈ R.
We prove the intermediate claim Happ: apply_fun uniform_metric_Romega p = Romega_uniform_metric_value (p 0) (p 1).
An exact proof term for the current goal is (apply_fun_graph (setprod real_sequences real_sequences) (λq : set ⇒ Romega_uniform_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 ∈ real_sequences.
An exact proof term for the current goal is (ap0_Sigma real_sequences (λ_ : set ⇒ real_sequences) p Hp).
We prove the intermediate claim Hp1: p 1 ∈ real_sequences.
An exact proof term for the current goal is (ap1_Sigma real_sequences (λ_ : set ⇒ real_sequences) p Hp).
An exact proof term for the current goal is (Romega_uniform_metric_value_in_R (p 0) (p 1) Hp0 Hp1).
∎