---

Step * of Lemma rv-mul-sep

∀rv:RealVectorSpace. ∀a,b:ℝ. ∀x,y:Point.  (a*x # b*y ⇒ (a ≠ b ∨ x # y))
BY
{ ((D 0 THENA Auto) THEN UseWitness ⌜rv."*sep"⌝⋅ THEN (D 1 THENA Auto) THEN RepUR ``rv-mul`` 0 THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}rv."*sep"\mkleeneclose{}\mcdot{}
  THEN  (D  1  THENA  Auto)
  THEN  RepUR  ``rv-mul``  0
  THEN  Trivial)

---

Home Index