theorem :: DBLSEQ_3:73

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 ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) iff for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty )