:: deftheorem defines convergent_in_cod2_to_+infty DBLSEQ_3:def 8 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_+infty iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_+infty );