:: deftheorem def34 defines cod1_major_iterated_lim DBLSEQ_1:def 7 :
for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod1 Rseq is convergent holds
for b₂ being Real holds
( b₂ = cod1_major_iterated_lim Rseq iff for e being Real st 0 < e holds
ex M being Nat st
for m being Nat st m >= M holds
|.(((lim_in_cod1 Rseq) . m) - b₂).| < e );