---

Step * of Lemma dim-qv-add

∀[as,bs:Top List].  dimension(qv-add(as;bs)) ~ dimension(as) supposing dimension(as) = dimension(bs) ∈ ℤ
BY
{ xxx(Unfold `qv-dim` 0
      THEN InductionOnList
      THEN RecUnfold `qv-add` 0
      THEN Reduce 0
      THEN ((UnivCD THENM EqCD THENM (BackThruSomeHyp ORELSE Trivial)) THENA Auto)
      THEN DVar `bs'
      THEN All Reduce
      THEN Auto')xxx }

---

Latex:

---

Latex:
\mforall{}[as,bs:Top  List].    dimension(qv-add(as;bs))  \msim{}  dimension(as)  supposing  dimension(as)  =  dimension(bs)


By

---

Latex:
xxx(Unfold  `qv-dim`  0
        THEN  InductionOnList
        THEN  RecUnfold  `qv-add`  0
        THEN  Reduce  0
        THEN  ((UnivCD  THENM  EqCD  THENM  (BackThruSomeHyp  ORELSE  Trivial))  THENA  Auto)
        THEN  DVar  `bs'
        THEN  All  Reduce
        THEN  Auto')xxx

---

Home Index