---

Step * 1 1 of Lemma rsum-single


1. n : ℤ
2. x : {i:ℤ| i = n ∈ ℤ}  ⟶ ℝ
⊢ radd-list([x[n]]) = x[n]
BY
{ ((RWO "radd-list-cons" 0 THENA Auto) THEN Reduce 0 THEN nRNorm 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  x  :  \{i:\mBbbZ{}|  i  =  n\}    {}\mrightarrow{}  \mBbbR{}
\mvdash{}  radd-list([x[n]])  =  x[n]


By

---

Latex:
((RWO  "radd-list-cons"  0  THENA  Auto)  THEN  Reduce  0  THEN  nRNorm  0  THEN  Auto)\mcdot{}

---

Home Index