---

Step * of Lemma sum-in-vs-single

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

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[K:Rng].  \mforall{}[vs:VectorSpace(K)].  \mforall{}[f:\{n..n  +  1\msupminus{}\}  {}\mrightarrow{}  Point(vs)].    (\mSigma{}\{f[i]  |  n\mleq{}i\mleq{}n\}  =  f[n])


By

---

Latex:
((Auto  THEN  Unfold  `sum-in-vs`  0)
  THEN  (Subst'  \mSigma{}\{f[i]  |  i  \mmember{}  [n,  n  +  1)\}  \msim{}  f[n]  +  0  0
              THENA  ((RecUnfold  `from-upto`  0  THEN  AutoSplit)
                            THEN  (CallByValueReduce  0  THENA  Auto)
                            THEN  RecUnfold  `from-upto`  0
                            THEN  AutoSplit
                            THEN  Computation)
              )
  THEN  Auto)

---

Home Index