---

Step * of Lemma series-sum-linear1

∀x,y:ℕ ⟶ ℝ. ∀a,b:ℝ.  (Σn.x[n] = a ⇒ Σn.y[n] = b ⇒ Σn.x[n] + y[n] = a + b)
BY
{ ((Unfold `series-sum` 0 THEN Auto)
   THEN FLemma `radd-limit` [-2;-1]
   THEN Auto
   THEN MoveToConcl (-1)
   THEN BLemma `converges-to_functionality`
   THEN Auto
   THEN RWO "rsum_linearity1" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Unfold  `series-sum`  0  THEN  Auto)
  THEN  FLemma  `radd-limit`  [-2;-1]
  THEN  Auto
  THEN  MoveToConcl  (-1)
  THEN  BLemma  `converges-to\_functionality`
  THEN  Auto
  THEN  RWO  "rsum\_linearity1"  0
  THEN  Auto)

---

Home Index