---

Step * of Lemma dim-qv-mul

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

---

Latex:

---

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


By

---

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

---

Home Index