theorem :: DBLSEQ_1:4

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