Set g to be the term (λp : set ⇒ mul_SNo (p 0) (p 1)).
We prove the intermediate claim Hg: ∀p : set, p ∈ setprod R R → g p ∈ R.
Let p be given.
Assume HpRR: p ∈ setprod R R.
We will prove g p ∈ R.
We prove the intermediate claim Hp0R: p 0 ∈ R.
An exact proof term for the current goal is (ap0_Sigma R (λ_ : set ⇒ R) p HpRR).
We prove the intermediate claim Hp1R: p 1 ∈ R.
An exact proof term for the current goal is (ap1_Sigma R (λ_ : set ⇒ R) p HpRR).
An exact proof term for the current goal is (real_mul_SNo (p 0) Hp0R (p 1) Hp1R).
We prove the intermediate claim Hdef: mul_fun_R = graph (setprod R R) g.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
An exact proof term for the current goal is (graph_in_function_space (setprod R R) R g Hg).
∎