---

Step * of Lemma real-vec-mul-cancel

∀[n:ℕ]. ∀[v:ℝ^n]. ∀[x,y:ℝ].  (v ≠ λi.r0 ⇒ x = y supposing req-vec(n;x*v;y*v))
BY
{ Auto }

1
1. n : ℕ
2. v : ℝ^n
3. x : ℝ
4. y : ℝ
5. v ≠ λi.r0
6. req-vec(n;x*v;y*v)
⊢ x = y

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[v:\mBbbR{}\^{}n].  \mforall{}[x,y:\mBbbR{}].    (v  \mneq{}  \mlambda{}i.r0  {}\mRightarrow{}  x  =  y  supposing  req-vec(n;x*v;y*v))


By

---

Latex:
Auto

---

Home Index