---

Step * of Lemma empty-sum-in-vs

∀[K:Rng]. ∀[vs:VectorSpace(K)]. ∀[n,m:ℤ]. ∀[f:Top].  Σ{f[i] | n≤i≤m} = 0 ∈ Point(vs) supposing m < n
BY
{ (Auto THEN Unfold `sum-in-vs` 0 THEN Subst' [n, m + 1) ~ {} 0 THEN Auto THEN RecUnfold `from-upto` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[K:Rng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[n,m:\mBbbZ{}].  \mforall{}[f:Top].    \mSigma{}\{f[i]  |  n\mleq{}i\mleq{}m\}  =  0  supposing  m  <  n


By

---

Latex:
(Auto
  THEN  Unfold  `sum-in-vs`  0
  THEN  Subst'  [n,  m  +  1)  \msim{}  \{\}  0
  THEN  Auto
  THEN  RecUnfold  `from-upto`  0
  THEN  AutoSplit)

---

Home Index