---

Step * of Lemma free-vs_wf

∀[S:Type]. ∀[K:CRng].  (free-vs(K;S) ∈ VectorSpace(K))
BY
{ (Auto
   THEN (Assert formal-sum(K;S) ∈ Type BY
               Auto)
   THEN (Assert bag(|K| × S) ⊆r formal-sum(K;S) BY
               (Fold `basic-formal-sum` 0 THEN Auto))
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[S:Type].  \mforall{}[K:CRng].    (free-vs(K;S)  \mmember{}  VectorSpace(K))


By

---

Latex:
(Auto
  THEN  (Assert  formal-sum(K;S)  \mmember{}  Type  BY
                          Auto)
  THEN  (Assert  bag(|K|  \mtimes{}  S)  \msubseteq{}r  formal-sum(K;S)  BY
                          (Fold  `basic-formal-sum`  0  THEN  Auto))
  THEN  ProveWfLemma)

---

Home Index