let Rseq, Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( 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) ) ) implies ( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 ) )
assume that
a1: ( Rseq1 is P-convergent & Rseq2 is P-convergent ) and
a2: P-lim Rseq1 = P-lim Rseq2 and
a3: for n, m being Nat holds
( Rseq1 . (n,m) <= Rseq . (n,m) & Rseq . (n,m) <= Rseq2 . (n,m) ) ; :: thesis: ( Rseq is P-convergent & P-lim Rseq = P-lim Rseq1 )
a4: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e )
assume a5: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e
then consider N1 being Nat such that
a6: for n, m being Nat st n >= N1 & m >= N1 holds
|.((Rseq1 . (n,m)) - (P-lim Rseq1)).| < e by a1, def6;
consider N2 being Nat such that
a7: for n, m being Nat st n >= N2 & m >= N2 holds
|.((Rseq2 . (n,m)) - (P-lim Rseq1)).| < e by a1, a2, a5, def6;
reconsider N = max (N1,N2) as Nat by TARSKI:1;
take N ; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - (P-lim Rseq1)).| < e
a8: ( max (N1,N2) >= N1 & max (N1,N2) >= N2 ) by XXREAL_0:25;

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.((Rseq . (n,m)) - (P-lim Rseq1)).| < e )
assume ( n >= N & m >= N ) ; :: thesis: |.((Rseq . (n,m)) - (P-lim Rseq1)).| < e
then ( n >= N1 & m >= N1 & n >= N2 & m >= N2 ) by a8, XXREAL_0:2;
then a9: ( |.((Rseq1 . (n,m)) - (P-lim Rseq1)).| < e & |.((Rseq2 . (n,m)) - (P-lim Rseq1)).| < e ) by a6, a7;
then a10: - e < - |.((Rseq1 . (n,m)) - (P-lim Rseq1)).| by XREAL_1:24;
- |.((Rseq1 . (n,m)) - (P-lim Rseq1)).| <= (Rseq1 . (n,m)) - (P-lim Rseq1) by ABSVALUE:4;
then a11: - e < (Rseq1 . (n,m)) - (P-lim Rseq1) by a10, XXREAL_0:2;
(Rseq2 . (n,m)) - (P-lim Rseq1) <= |.((Rseq2 . (n,m)) - (P-lim Rseq1)).| by ABSVALUE:4;
then a12: (Rseq2 . (n,m)) - (P-lim Rseq1) < e by a9, XXREAL_0:2;
a13: ( (Rseq1 . (n,m)) - (P-lim Rseq1) <= (Rseq . (n,m)) - (P-lim Rseq1) & (Rseq . (n,m)) - (P-lim Rseq1) <= (Rseq2 . (n,m)) - (P-lim Rseq1) ) by a3, XREAL_1:9;
then ( - e < (Rseq . (n,m)) - (P-lim Rseq1) & (Rseq . (n,m)) - (P-lim Rseq1) < e ) by a11, a12, XXREAL_0:2;
then a14: |.((Rseq . (n,m)) - (P-lim Rseq1)).| <= e by ABSVALUE:5;
- ((Rseq . (n,m)) - (P-lim Rseq1)) <> e by a3, a11, XREAL_1:9;
then |.((Rseq . (n,m)) - (P-lim Rseq1)).| <> e by a13, a12, ABSVALUE:1;
hence |.((Rseq . (n,m)) - (P-lim Rseq1)).| < e by a14, XXREAL_0:1; :: thesis: verum

end;

end;

hence Rseq is P-convergent ; :: thesis: P-lim Rseq = P-lim Rseq1
hence P-lim Rseq = P-lim Rseq1 by a4, def6; :: thesis: verum