Let p be given.
Assume Hp: p ∈ setprod R R.
We will prove apply_fun mul_fun_R p ∈ R.
rewrite the current goal using (apply_fun_graph (setprod R R) (λp0 : set ⇒ mul_SNo (p0 0) (p0 1)) p Hp) (from left to right).
We prove the intermediate claim Hp0R: p 0 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p Hp).
We prove the intermediate claim Hp1R: p 1 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p Hp).
An exact proof term for the current goal is (real_mul_SNo (p 0) Hp0R (p 1) Hp1R).
∎