---

Step * of Lemma dot-product_wf

∀[n:ℕ]. ∀[x,y:ℝ^n].  (x ⋅ y ∈ ℝ)
BY
{ (Unfold `real-vec` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (x  \mcdot{}  y  \mmember{}  \mBbbR{})


By

---

Latex:
(Unfold  `real-vec`  0  THEN  ProveWfLemma)

---

Home Index