---

Step * of Lemma isolate_summand2

No Annotations
∀m:ℕ. ∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  Σ(f[x] | x < n) = (f[m] + Σ(if (x =z m) then 0 else f[x] fi  | x < n)) ∈ ℤ supposing m < n
BY
{ Auto }

---

Latex:

---

Latex:
No  Annotations
\mforall{}m:\mBbbN{}
    \mforall{}[n:\mBbbN{}].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
        \mSigma{}(f[x]  |  x  <  n)  =  (f[m]  +  \mSigma{}(if  (x  =\msubz{}  m)  then  0  else  f[x]  fi    |  x  <  n))  supposing  m  <  n


By

---

Latex:
Auto

---

Home Index