theorem :: DBLSEQ_3:29

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