theorem Th74: :: DBLSEQ_3:74

for f being nonnegative Function of [:NAT,NAT:],ExtREAL
for m being Nat holds
( (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) )