---

Step * of Lemma rmul*_functionality

∀[x,y,u,v:ℝ*].  (x = y ⇒ u = v ⇒ x * u = y * v)
BY
{ (Intros
   THEN Unfold `rmul*` 0
   THEN RWO "-1 -2" 0
   THEN Auto
   THEN ((Reduce 0 THEN RWO "-1 -2" 0 THEN Auto) ORELSE (Fold `rmul*` 0 THEN RelRST THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[x,y,u,v:\mBbbR{}*].    (x  =  y  {}\mRightarrow{}  u  =  v  {}\mRightarrow{}  x  *  u  =  y  *  v)


By

---

Latex:
(Intros
  THEN  Unfold  `rmul*`  0
  THEN  RWO  "-1  -2"  0
  THEN  Auto
  THEN  ((Reduce  0  THEN  RWO  "-1  -2"  0  THEN  Auto)  ORELSE  (Fold  `rmul*`  0  THEN  RelRST  THEN  Auto)))

---

Home Index