:: deftheorem D1DEF6 defines lim_in_cod2 DBLSEQ_3:def 13 :
for f being Function of [:NAT,NAT:],ExtREAL
for b₂ being ExtREAL_sequence holds
( b₂ = lim_in_cod2 f iff for n being Element of NAT holds b₂ . n = lim (ProjMap1 (f,n)) );