:: deftheorem defines convergent_in_cod1 DBLSEQ_3:def 7 :
for f being Function of [:NAT,NAT:],ExtREAL holds
( f is convergent_in_cod1 iff for m being Element of NAT holds ProjMap2 (f,m) is convergent );