:: deftheorem def35 defines cod2_major_iterated_lim DBLSEQ_1:def 8 :
for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds
for b₂ being Real holds
( b₂ = cod2_major_iterated_lim Rseq iff for e being Real st 0 < e holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((lim_in_cod2 Rseq) . n) - b₂).| < e );