let Rseq1, Rseq2 be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq1 is P-convergent & Rseq2 is P-convergent implies ( Rseq1 - Rseq2 is P-convergent & P-lim (Rseq1 - Rseq2) = (P-lim Rseq1) - (P-lim Rseq2) ) )
assume a1: ( Rseq1 is P-convergent & Rseq2 is P-convergent ) ; :: thesis: ( Rseq1 - Rseq2 is P-convergent & P-lim (Rseq1 - Rseq2) = (P-lim Rseq1) - (P-lim Rseq2) )
a2: now :: thesis: for e being Real st 0 < e holds
ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e
let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e )
assume a4: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e
then consider N1 being Nat such that
a5: for n, m being Nat st n >= N1 & m >= N1 holds
|.((Rseq1 . (n,m)) - (P-lim Rseq1)).| < e / 2 by a1, def6;
consider N2 being Nat such that
a6: for n, m being Nat st n >= N2 & m >= N2 holds
|.((Rseq2 . (n,m)) - (P-lim Rseq2)).| < e / 2 by a1, a4, def6;
reconsider N = max (N1,N2) as Nat by TARSKI:1;
take N = N; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e
now :: thesis: for n, m being Nat st n >= N & m >= N holds
|.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e
let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e )
assume a8: ( n >= N & m >= N ) ; :: thesis: |.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e
( N >= N1 & N >= N2 ) by XXREAL_0:25;
then ( n >= N1 & n >= N2 & m >= N1 & m >= N2 ) by a8, XXREAL_0:2;
then a10: ( |.((Rseq1 . (n,m)) - (P-lim Rseq1)).| < e / 2 & |.((Rseq2 . (n,m)) - (P-lim Rseq2)).| < e / 2 ) by a5, a6;
then |.((P-lim Rseq2) - (Rseq2 . (n,m))).| < e / 2 by COMPLEX1:60;
then a9: |.((Rseq1 . (n,m)) - (P-lim Rseq1)).| + |.((P-lim Rseq2) - (Rseq2 . (n,m))).| < (e / 2) + (e / 2) by a10, XREAL_1:8;
(Rseq1 - Rseq2) . (n,m) = (Rseq1 . (n,m)) - (Rseq2 . (n,m)) by lmADD;
then ((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2)) = ((Rseq1 . (n,m)) - (P-lim Rseq1)) + ((P-lim Rseq2) - (Rseq2 . (n,m))) ;
then |.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| <= |.((Rseq1 . (n,m)) - (P-lim Rseq1)).| + |.((P-lim Rseq2) - (Rseq2 . (n,m))).| by COMPLEX1:56;
hence |.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e by a9, XXREAL_0:2; :: thesis: verum
end;
hence for n, m being Nat st n >= N & m >= N holds
|.(((Rseq1 - Rseq2) . (n,m)) - ((P-lim Rseq1) - (P-lim Rseq2))).| < e ; :: thesis: verum
end;
hence Rseq1 - Rseq2 is P-convergent ; :: thesis: P-lim (Rseq1 - Rseq2) = (P-lim Rseq1) - (P-lim Rseq2)
hence P-lim (Rseq1 - Rseq2) = (P-lim Rseq1) - (P-lim Rseq2) by a2, def6; :: thesis: verum