theorem :: DBLSEQ_1:6

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