:: deftheorem D1DEF5 defines lim_in_cod1 DBLSEQ_3:def 12 :
for f being Function of [:NAT,NAT:],ExtREAL
for b₂ being ExtREAL_sequence holds
( b₂ = lim_in_cod1 f iff for m being Element of NAT holds b₂ . m = lim (ProjMap2 (f,m)) );