theorem Th77: :: DBLSEQ_3:77

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