theorem Th35: :: MEASURE9:37

for F being without-infty FinSequence of ExtREAL
for G being ExtREAL_sequence st ( for i being Nat holds F . i = G . i ) holds
for i being Nat holds Sum (F | i) = (Partial_Sums G) . i