Let c be given.

Assume HcR: c ∈ R.

Set g to be the term (λt : set ⇒ mul_SNo t c).

We prove the intermediate claim Hg: ∀t : set, t ∈ R → g t ∈ R.

Let t be given.

Assume HtR: t ∈ R.

We will prove g t ∈ R.

An exact proof term for the current goal is (real_mul_SNo t HtR c HcR).

We prove the intermediate claim Hdef: mul_const_fun c = graph 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 R R g Hg).

∎