---

Step * of Lemma rv-mul-sep1

∀rv:RealVectorSpace. ∀a,b:ℝ. ∀y:Point.  (a*y # b*y ⇒ a ≠ b)
BY
{ (InstLemma `rv-mul-sep` []
   THEN ParallelLast'
   THEN Auto
   THEN (FHyp 2 [-1] THENM D -1)
   THEN Auto
   THEN (Assert ¬y # y BY
               Auto)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:RealVectorSpace.  \mforall{}a,b:\mBbbR{}.  \mforall{}y:Point.    (a*y  \#  b*y  {}\mRightarrow{}  a  \mneq{}  b)


By

---

Latex:
(InstLemma  `rv-mul-sep`  []
  THEN  ParallelLast'
  THEN  Auto
  THEN  (FHyp  2  [-1]  THENM  D  -1)
  THEN  Auto
  THEN  (Assert  \mneg{}y  \#  y  BY
                          Auto)
  THEN  Auto)

---

Home Index