:: deftheorem defines convergent_in_cod2 DBLSEQ_1:def 4 :
for Rseq being Function of [:NAT,NAT:],REAL holds
( Rseq is convergent_in_cod2 iff for n being Element of NAT holds ProjMap1 (Rseq,n) is convergent );