---

Step * 1 1 1 1 of Lemma partition-sum-constant

.....equality..... 
1. I : Interval
2. icompact(I)
3. c : ℝ
4. p : partition(I)
5. y : partition-choice(full-partition(I;p))
6. v : ℝ List
7. full-partition(I;p) = v ∈ (ℝ List)
8. 1 < ||v||
⊢ (last(v) - v[0]) = |I| ∈ ℝ
BY
{ (StrongRevHypSubst (-2) 0 THENA (Auto THEN Subst' z = v ∈ (ℝ List) 0 THEN Auto)) }

1
1. I : Interval
2. icompact(I)
3. c : ℝ
4. p : partition(I)
5. y : partition-choice(full-partition(I;p))
6. v : ℝ List
7. full-partition(I;p) = v ∈ (ℝ List)
8. 1 < ||v||
⊢ (last(full-partition(I;p)) - full-partition(I;p)[0]) = |I| ∈ ℝ

---

Latex:

---

Latex:
.....equality..... 
1.  I  :  Interval
2.  icompact(I)
3.  c  :  \mBbbR{}
4.  p  :  partition(I)
5.  y  :  partition-choice(full-partition(I;p))
6.  v  :  \mBbbR{}  List
7.  full-partition(I;p)  =  v
8.  1  <  ||v||
\mvdash{}  (last(v)  -  v[0])  =  |I|


By

---

Latex:
(StrongRevHypSubst  (-2)  0  THENA  (Auto  THEN  Subst'  z  =  v  0  THEN  Auto))

---

Home Index