theorem Th91: :: DBLSEQ_3:91

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for seq being ExtREAL_sequence st ( for m being Element of NAT holds
( ProjMap2 (f,m) is non-decreasing & seq . m = lim (ProjMap2 (f,m)) ) ) holds
( lim_in_cod2 (Partial_Sums_in_cod2 f) is non-decreasing & Sum seq = lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) )