:: deftheorem defines convergent_in_cod1 DBLSEQ_1:def 3 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is convergent_in_cod1 iff for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent );