theorem Th1: :: MEASURE8:1

for seq being ExtREAL_sequence holds Ser seq = Partial_Sums seq