---

Step * of Lemma dot-product_functionality

∀[n:ℕ]. ∀[x1,y1,x2,y2:ℝ^n].  (x1 ⋅ y1 = x2 ⋅ y2) supposing (req-vec(n;x1;x2) and req-vec(n;y1;y2))
BY
{ (RepUR ``real-vec req-vec dot-product`` 0 THEN Auto THEN RWO "-1 -2" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x1,y1,x2,y2:\mBbbR{}\^{}n].    (x1  \mcdot{}  y1  =  x2  \mcdot{}  y2)  supposing  (req-vec(n;x1;x2)  and  req-vec(n;y1;y2))


By

---

Latex:
(RepUR  ``real-vec  req-vec  dot-product``  0  THEN  Auto  THEN  RWO  "-1  -2"  0  THEN  Auto)

---

Home Index