---

Step * of Lemma series-sum_functionality

∀x,y:ℕ ⟶ ℝ. ∀a,b:ℝ.  ({Σn.x[n] = a ⇒ Σn.y[n] = b}) supposing ((a = b) and (∀n:ℕ. (x[n] = y[n])))
BY
{ ((UnivCD THENA Auto) THEN Unfold `series-sum` 0 THEN BLemma `converges-to_functionality` THEN Auto) }

1
1. x : ℕ ⟶ ℝ
2. y : ℕ ⟶ ℝ
3. a : ℝ
4. b : ℝ
5. ∀n:ℕ. (x[n] = y[n])
6. a = b
7. n : ℕ
⊢ Σ{x[i] | 0≤i≤n} = Σ{y[i] | 0≤i≤n}

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a,b:\mBbbR{}.    (\{\mSigma{}n.x[n]  =  a  {}\mRightarrow{}  \mSigma{}n.y[n]  =  b\})  supposing  ((a  =  b)  and  (\mforall{}n:\mBbbN{}.  (x[n]  =  y[n])))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `series-sum`  0  THEN  BLemma  `converges-to\_functionality`  THEN  Auto)

---

Home Index