---

Step * of Lemma series-sum-unique

∀[x:ℕ ⟶ ℝ]. ∀[a,b:ℝ].  (a = b) supposing (Σn.x[n] = b and Σn.x[n] = a)
BY
{ ((Unfold `series-sum` 0 THEN Auto) THEN FLemma `unique-limit` [-1;-2] THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Unfold  `series-sum`  0  THEN  Auto)  THEN  FLemma  `unique-limit`  [-1;-2]  THEN  Auto)

---

Home Index