theorem Th72: :: DBLSEQ_3:72

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