theorem :: DBLSEQ_1:3

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is P-convergent & Rseq is convergent_in_cod2 holds
P-lim Rseq = cod2_major_iterated_lim Rseq