let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( lim_in_cod1 Rseq is convergent implies cod1_major_iterated_lim Rseq = lim (lim_in_cod1 Rseq) )
assume A1: lim_in_cod1 Rseq is convergent ; :: thesis: cod1_major_iterated_lim Rseq = lim (lim_in_cod1 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_cod1 Rseq) . m) - g).| < p by SEQ_2:def 6;
g = lim (lim_in_cod1 Rseq) by A1, A2, SEQ_2:def 7;
hence cod1_major_iterated_lim Rseq = lim (lim_in_cod1 Rseq) by A1, A2, DBLSEQ_1:def 7; :: thesis: verum