:: deftheorem def33 defines lim_in_cod2 DBLSEQ_1:def 6 :
for Rseq being Function of [:NAT,NAT:],REAL
for b₂ being Function of NAT,REAL holds
( b₂ = lim_in_cod2 Rseq iff for n being Element of NAT holds b₂ . n = lim (ProjMap1 (Rseq,n)) );