let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Partial_Sums Rseq is P-convergent implies ( Rseq is P-convergent & P-lim Rseq = 0 ) )
set CPS = Partial_Sums Rseq;
assume A1: Partial_Sums Rseq is P-convergent ; :: thesis: ( Rseq is P-convergent & P-lim Rseq = 0 )
set Plim = P-lim (Partial_Sums Rseq);
a2: 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)) - 0).| < 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)) - 0).| < e )
assume A3: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - 0).| < e
set e1 = e / 4;
consider N being Nat such that
a4: for n, m being Nat st n >= N & m >= N holds
|.(((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq))).| < e / 4 by A1, A3, DBLSEQ_1:def 2;
take N1 = N + 1; :: thesis: for n, m being Nat st n >= N1 & m >= N1 holds
|.((Rseq . (n,m)) - 0).| < e

hereby :: thesis: verum

let n1, m1 be Nat; :: thesis: ( n1 >= N1 & m1 >= N1 implies |.((Rseq . (n1,m1)) - 0).| < e )
assume A5: ( n1 >= N1 & m1 >= N1 ) ; :: thesis: |.((Rseq . (n1,m1)) - 0).| < e
then a5: ( n1 > N & m1 > N ) by NAT_1:13;
then reconsider n = n1 - 1, m = m1 - 1 as Element of NAT by NAT_1:20;
a6: ( n1 = n + 1 & m1 = m + 1 ) ;
( n + 1 > N & m + 1 > N ) by A5, NAT_1:13;
then a7: ( n >= N & m >= N ) by NAT_1:13;
Rseq . (n1,m1) = ((((Partial_Sums Rseq) . (n1,m1)) - ((Partial_Sums Rseq) . (n,m1))) - ((Partial_Sums Rseq) . (n1,m))) + ((Partial_Sums Rseq) . (n,m)) by a6, thRS2
.= ((((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq)))) - ((((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq)))) ;
then a8: |.((Rseq . (n1,m1)) - 0).| <= |.((((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq)))).| + |.((((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq)))).| by COMPLEX1:57;
a9: |.((((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq)))).| <= |.(((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))).| + |.(((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq))).| by COMPLEX1:57;
a10: |.((((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq)))).| <= |.(((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))).| + |.(((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq))).| by COMPLEX1:57;
( |.(((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))).| < e / 4 & |.(((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))).| < e / 4 & |.(((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq))).| < e / 4 & |.(((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq))).| < e / 4 ) by a4, a5, a7;
then ( |.(((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))).| + |.(((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq))).| < (e / 4) + (e / 4) & |.(((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))).| + |.(((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq))).| < (e / 4) + (e / 4) ) by XREAL_1:8;
then ( |.((((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq)))).| < (e / 4) + (e / 4) & |.((((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq)))).| < (e / 4) + (e / 4) ) by a9, a10, XXREAL_0:2;
then |.((((Partial_Sums Rseq) . (n1,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n1,m)) - (P-lim (Partial_Sums Rseq)))).| + |.((((Partial_Sums Rseq) . (n,m1)) - (P-lim (Partial_Sums Rseq))) - (((Partial_Sums Rseq) . (n,m)) - (P-lim (Partial_Sums Rseq)))).| < ((e / 4) + (e / 4)) + ((e / 4) + (e / 4)) by XREAL_1:8;
hence |.((Rseq . (n1,m1)) - 0).| < e by a8, XXREAL_0:2; :: thesis: verum

end;

end;

hence Rseq is P-convergent ; :: thesis: P-lim Rseq = 0
hence P-lim Rseq = 0 by a2, DBLSEQ_1:def 2; :: thesis: verum