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