---

Step * of Lemma r3-dot-product

∀[a,b:ℝ^3].  (a⋅b = (((a 0) * (b 0)) + ((a 1) * (b 1)) + ((a 2) * (b 2))))
BY
{ (Auto
   THEN RepUR ``dot-product`` 0
   THEN RepeatFor 2 (((RWO "rsum-split-first" 0 THENA Auto) THEN Reduce 0))
   THEN RWO "rsum-single" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}\^{}3].    (a\mcdot{}b  =  (((a  0)  *  (b  0))  +  ((a  1)  *  (b  1))  +  ((a  2)  *  (b  2))))


By

---

Latex:
(Auto
  THEN  RepUR  ``dot-product``  0
  THEN  RepeatFor  2  (((RWO  "rsum-split-first"  0  THENA  Auto)  THEN  Reduce  0))
  THEN  RWO  "rsum-single"  0
  THEN  Auto)

---

Home Index