---

Step * of Lemma rv-mul-sep2

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

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rv-mul-sep`  []
  THEN  ParallelLast'
  THEN  Auto
  THEN  (FHyp  2  [-1]  THENM  D  -1)
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index