theorem :: DBLSEQ_3:71

for f being without-infty Function of [:NAT,NAT:],ExtREAL st Partial_Sums f is convergent_in_cod1_to_-infty holds
ex m being Element of NAT st ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_-infty