---

Step * of Lemma rmul-rinv

∀[x:ℝ]. (x * rinv(x)) = r1 supposing x ≠ r0
BY
{ EAuto 2 }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (x  *  rinv(x))  =  r1  supposing  x  \mneq{}  r0


By

---

Latex:
EAuto  2

---

Home Index