---

Step * of Lemma rmul-distrib2

∀[x,y,z:ℝ].  (((y + z) * x) = ((y * x) + (z * x)))
BY
{ (Auto THEN RWO "rmul_comm" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y,z:\mBbbR{}].    (((y  +  z)  *  x)  =  ((y  *  x)  +  (z  *  x)))


By

---

Latex:
(Auto  THEN  RWO  "rmul\_comm"  0  THEN  Auto)

---

Home Index