:: deftheorem def32 defines lim_in_cod1 DBLSEQ_1:def 5 :
for Rseq being Function of [:NAT,NAT:],REAL
for b₂ being Function of NAT,REAL holds
( b₂ = lim_in_cod1 Rseq iff for m being Element of NAT holds b₂ . m = lim (ProjMap2 (Rseq,m)) );