Let p be given.

Assume HpRR: p ∈ setprod R R.

We will prove apply_fun mul_fun_R p = mul_SNo (p 0) (p 1).

We prove the intermediate claim Hdef: mul_fun_R = graph (setprod R R) (λp0 : set ⇒ mul_SNo (p0 0) (p0 1)).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

rewrite the current goal using (apply_fun_graph (setprod R R) (λp0 : set ⇒ mul_SNo (p0 0) (p0 1)) p HpRR) (from left to right).

Use reflexivity.

∎