theorem Th79: :: DBLSEQ_3:79

for f being without-infty Function of [:NAT,NAT:],ExtREAL holds
( Partial_Sums f is convergent_in_cod1_to_finite iff Partial_Sums_in_cod1 f is convergent_in_cod1_to_finite )