theorem Th9: :: PROB_4:9

for seq being sequence of REAL
for Eseq being sequence of ExtREAL st seq = Eseq holds
Partial_Sums seq = Ser Eseq