:: deftheorem defines convergent_in_cod2_to_finite DBLSEQ_3:def 10 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod2_to_finite iff for m being Element of NAT holds ProjMap1 (f,m) is convergent_to_finite_number );