let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is P-convergent iff Rseq is Cauchy )

hereby :: thesis: ( Rseq is Cauchy implies Rseq is P-convergent )

assume a1: Rseq is P-convergent ; :: thesis: Rseq is Cauchy

now :: thesis: for e being Real st e > 0 holds
ex N being Nat st
for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e

let e be Real; :: thesis: ( e > 0 implies ex N being Nat st
for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e )
assume a2: e > 0 ; :: thesis: ex N being Nat st
for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e
consider z being Real such that
a3: 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)) - z).| < e by a1;
consider N being Nat such that
a4: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - z).| < e / 2 by a2, a3;

now :: thesis: for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e

let n1, n2, m1, m2 be Nat; :: thesis: ( N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 implies |.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e )
assume b1: ( N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 ) ; :: thesis: |.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e
then ( N <= n2 & N <= m2 ) by XXREAL_0:2;
then ( |.((Rseq . (n1,m1)) - z).| < e / 2 & |.((Rseq . (n2,m2)) - z).| < e / 2 ) by a4, b1;
then |.((Rseq . (n2,m2)) - z).| + |.((Rseq . (n1,m1)) - z).| < (e / 2) + (e / 2) by XREAL_1:8;
then a5: |.((Rseq . (n2,m2)) - z).| + |.(z - (Rseq . (n1,m1))).| < e by COMPLEX1:60;
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| <= |.((Rseq . (n2,m2)) - z).| + |.(z - (Rseq . (n1,m1))).| by COMPLEX1:63;
hence |.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e by a5, XXREAL_0:2; :: thesis: verum

end;

hence ex N being Nat st
for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e ; :: thesis: verum

end;

hence Rseq is Cauchy ; :: thesis: verum

end;

assume a6: Rseq is Cauchy ; :: thesis: Rseq is P-convergent
deffunc H₁( Element of NAT ) -> Element of REAL = Rseq . ($1,$1);
consider seq being Function of NAT,REAL such that
a7: for n being Element of NAT holds seq . n = H₁(n) from FUNCT_2:sch 4();
reconsider seq = seq as Real_Sequence ;

now :: thesis: for e being Real st e > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.((seq . n) - (seq . N)).| < e

let e be Real; :: thesis: ( e > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.((seq . n) - (seq . N)).| < e )
assume e > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.((seq . n) - (seq . N)).| < e
then consider N being Nat such that
a8: for n1, n2, m1, m2 being Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e by a6;
take N = N; :: thesis: for n being Nat st n >= N holds
|.((seq . n) - (seq . N)).| < e

hereby :: thesis: verum

let n be Nat; :: thesis: ( n >= N implies |.((seq . n) - (seq . N)).| < e )
c1: ( n is Element of NAT & N is Element of NAT ) by ORDINAL1:def 12;
assume n >= N ; :: thesis: |.((seq . n) - (seq . N)).| < e
then |.((Rseq . (n,n)) - (Rseq . (N,N))).| < e by a8;
then |.((seq . n) - (Rseq . (N,N))).| < e by a7, c1;
hence |.((seq . n) - (seq . N)).| < e by a7, c1; :: thesis: verum

end;

end;

then a11: seq is convergent by SEQ_4:41;
reconsider z = lim seq as Complex ;
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)) - z).| < 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)) - z).| < e )
assume a12: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - z).| < e
then consider N1 being Nat such that
a13: for n being Nat st n >= N1 holds
|.((seq . n) - (lim seq)).| < e / 2 by a11, SEQ_2:def 7;
consider N2 being Nat such that
a14: for n1, n2, m1, m2 being Nat st N2 <= n1 & n1 <= n2 & N2 <= m1 & m1 <= m2 holds
|.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e / 2 by a6, a12;
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)) - z).| < e

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.((Rseq . (n,m)) - z).| < e )
c2: N is Element of NAT by ORDINAL1:def 12;
assume a15: ( n >= N & m >= N ) ; :: thesis: |.((Rseq . (n,m)) - z).| < e
a18: Rseq . (N,N) = seq . N by a7, c2;
( N >= N1 & N >= N2 ) by XXREAL_0:25;
then ( |.((Rseq . (N,N)) - z).| < e / 2 & |.((Rseq . (n,m)) - (Rseq . (N,N))).| < e / 2 ) by a13, a14, a18, a15;
then b1: |.((Rseq . (n,m)) - (Rseq . (N,N))).| + |.((Rseq . (N,N)) - z).| < (e / 2) + (e / 2) by XREAL_1:8;
|.((Rseq . (n,m)) - z).| <= |.((Rseq . (n,m)) - (Rseq . (N,N))).| + |.((Rseq . (N,N)) - z).| by COMPLEX1:63;
hence |.((Rseq . (n,m)) - z).| < e by b1, XXREAL_0:2; :: thesis: verum

end;

end;

hence Rseq is P-convergent ; :: thesis: verum