theorem :: DBLSEQ_1:16

for Rseq, Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is P-convergent & Rseq2 is P-convergent & P-lim Rseq1 = P-lim Rseq2 & ( for n, m being Nat holds
( Rseq1 . (n,m) <= Rseq . (n,m) & Rseq . (n,m) <= Rseq2 . (n,m) ) ) holds
( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 )