theorem Th36: :: MEASUR10:35

for f being V169() FinSequence of ExtREAL
for s being V169() ExtREAL_sequence st ( for n being object st n in dom f holds
f . n = s . n ) holds
(Sum f) + (s . 0) = (Partial_Sums s) . (len f)