---

Step * of Lemma select-qv-mul

∀[as:Top List]. ∀[r:Top]. ∀[i:ℕdimension(as)].  (qv-mul(r;as)[i] ~ r * as[i])
BY
{ (Unfold `qv-dim` 0 THEN (Auto THEN Unfold `qv-mul` 0 THEN (RWO "select-map" 0 THENA Auto) THEN Reduce 0 THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[as:Top  List].  \mforall{}[r:Top].  \mforall{}[i:\mBbbN{}dimension(as)].    (qv-mul(r;as)[i]  \msim{}  r  *  as[i])


By

---

Latex:
(Unfold  `qv-dim`  0
  THEN  (Auto  THEN  Unfold  `qv-mul`  0  THEN  (RWO  "select-map"  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)
  )

---

Home Index