theorem :: DBLSEQ_3:30

for Rseq being Function of [:NAT,NAT:],REAL st lim_in_cod2 Rseq is convergent holds
cod2_major_iterated_lim Rseq = lim (lim_in_cod2 Rseq)