theorem :: DBLSEQ_3:75

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