let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( lim_in_cod2 Rseq is convergent implies cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq) )
assume A1: lim_in_cod2 Rseq is convergent ; :: thesis: cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq)
then consider g being Real such that
A2: for p being Real st 0 < p holds
ex M being Nat st
for m being Nat st M <= m holds
|.(((lim_in_cod2 Rseq) . m) - g).| < p by SEQ_2:def 6;
g = lim (lim_in_cod2 Rseq) by A1, A2, SEQ_2:def 7;
hence cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq) by A1, A2, DBLSEQ_1:def 8; :: thesis: verum