dblseq_1.miz

begin

 reserve Rseq,Rseq1,Rseq2 for Function of [: NAT , NAT :], REAL ;

 reserve rseq1,rseq2 for convergent Real_Sequence;

 reserve n,m,N,M for Nat;

 reserve e,r for Real;

 definition

 let Rseq;

 :: DBLSEQ_1:def1

 attr Rseq is P-convergent means ex p be Real st for e be Real st 0 < e holds ex N be Nat st for n,m be Nat st n >= N & m >= N holds |.((Rseq . (n,m)) - p).| < e;

 end

 definition

 let Rseq;

 assume

 A1: Rseq is P-convergent;

 :: DBLSEQ_1:def2

 func P-lim Rseq -> Real means

 : def6: for e be Real st 0 < e holds ex N be Nat st for n,m be Nat st n >= N & m >= N holds |.((Rseq . (n,m)) - it ).| < e;

 existence by A1;

 uniqueness

 proof

 given g1,g2 be Real such that

 A2: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - g1).| < e and

 A3: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - g2).| < e and

 A4: g1 <> g2;

 A5:

 now

 assume |.(g1 - g2).| = 0 ;

 then (g1 - g2) = 0 by ABSVALUE: 2;

 hence contradiction by A4;

 end;



 A6: 0 <= |.(g1 - g2).| by COMPLEX1: 46;

 then

 consider N1 be Nat such that

 A7: for n, m st N1 <= n & N1 <= m holds |.((Rseq . (n,m)) - g1).| < ( |.(g1 - g2).| / 4) by A2, A5;

 consider N2 be Nat such that

 A8: for n, m st N2 <= n & N2 <= m holds |.((Rseq . (n,m)) - g2).| < ( |.(g1 - g2).| / 4) by A3, A5, A6;

 (N1 + N2) >= N1 & (N1 + N2) >= N2 by NAT_1: 11;

 then |.((Rseq . ((N1 + N2),(N1 + N2))) - g1).| < ( |.(g1 - g2).| / 4) & |.((Rseq . ((N1 + N2),(N1 + N2))) - g2).| < ( |.(g1 - g2).| / 4) by A7, A8;

 then

 A10: ( |.((Rseq . ((N1 + N2),(N1 + N2))) - g2).| + |.((Rseq . ((N1 + N2),(N1 + N2))) - g1).|) < (( |.(g1 - g2).| / 4) + ( |.(g1 - g2).| / 4)) by XREAL_1: 8;

 |.(g1 - g2).| = |.(( - ((Rseq . ((N1 + N2),(N1 + N2))) - g1)) + ((Rseq . ((N1 + N2),(N1 + N2))) - g2)).|;

 then |.(g1 - g2).| <= ( |.( - ((Rseq . ((N1 + N2),(N1 + N2))) - g1)).| + |.((Rseq . ((N1 + N2),(N1 + N2))) - g2).|) by COMPLEX1: 56;

 then

 A11: |.(g1 - g2).| <= ( |.((Rseq . ((N1 + N2),(N1 + N2))) - g1).| + |.((Rseq . ((N1 + N2),(N1 + N2))) - g2).|) by COMPLEX1: 52;

 ( |.(g1 - g2).| / 2) < |.(g1 - g2).| by A5, A6, XREAL_1: 216;

 hence contradiction by A10, A11, XXREAL_0: 2;

 end;

 end

 definition

 let Rseq;

 :: DBLSEQ_1:def3

 attr Rseq is convergent_in_cod1 means for m be Element of NAT holds ( ProjMap2 (Rseq,m)) is convergent;

 :: DBLSEQ_1:def4

 attr Rseq is convergent_in_cod2 means for n be Element of NAT holds ( ProjMap1 (Rseq,n)) is convergent;

 end

 definition

 let Rseq;

 :: DBLSEQ_1:def5

 func lim_in_cod1 Rseq -> Function of NAT , REAL means

 : def32: for m be Element of NAT holds (it . m) = ( lim ( ProjMap2 (Rseq,m)));

 existence

 proof

 defpred P[ Element of NAT , set] means $2 = ( lim ( ProjMap2 (Rseq,$1)));

 a1:

 now

 let m be Element of NAT ;

 reconsider n = ( lim ( ProjMap2 (Rseq,m))) as Element of REAL by XREAL_0:def 1;

 take n;

 thus P[m, n];

 end;

 consider IT be Function of NAT , REAL such that

 a2: for m be Element of NAT holds P[m, (IT . m)] from FUNCT_2:sch 3( a1);

 take IT;

 thus thesis by a2;

 end;

 uniqueness

 proof

 let f1,f2 be Function of NAT , REAL ;

 assume that

 a3: for m be Element of NAT holds (f1 . m) = ( lim ( ProjMap2 (Rseq,m))) and

 a4: for m be Element of NAT holds (f2 . m) = ( lim ( ProjMap2 (Rseq,m)));

 now

 let m be Element of NAT ;



 thus (f1 . m) = ( lim ( ProjMap2 (Rseq,m))) by a3

 .= (f2 . m) by a4;

 end;

 hence f1 = f2 by FUNCT_2: 63;

 end;

 end

 definition

 let Rseq;

 :: DBLSEQ_1:def6

 func lim_in_cod2 Rseq -> Function of NAT , REAL means

 : def33: for n be Element of NAT holds (it . n) = ( lim ( ProjMap1 (Rseq,n)));

 existence

 proof

 defpred P[ Element of NAT , set] means $2 = ( lim ( ProjMap1 (Rseq,$1)));

 a1:

 now

 let m be Element of NAT ;

 reconsider n = ( lim ( ProjMap1 (Rseq,m))) as Element of REAL by XREAL_0:def 1;

 take n;

 thus P[m, n];

 end;

 consider IT be Function of NAT , REAL such that

 a2: for m be Element of NAT holds P[m, (IT . m)] from FUNCT_2:sch 3( a1);

 take IT;

 thus thesis by a2;

 end;

 uniqueness

 proof

 let f1,f2 be Function of NAT , REAL ;

 assume that

 a3: for n be Element of NAT holds (f1 . n) = ( lim ( ProjMap1 (Rseq,n))) and

 a4: for n be Element of NAT holds (f2 . n) = ( lim ( ProjMap1 (Rseq,n)));

 now

 let n be Element of NAT ;



 thus (f1 . n) = ( lim ( ProjMap1 (Rseq,n))) by a3

 .= (f2 . n) by a4;

 end;

 hence f1 = f2 by FUNCT_2: 63;

 end;

 end

 definition

 let Rseq;

 assume

 a2: ( lim_in_cod1 Rseq) is convergent;

 :: DBLSEQ_1:def7

 func cod1_major_iterated_lim Rseq -> Real means

 : def34: for e be Real st 0 < e holds ex M be Nat st for m be Nat st m >= M holds |.((( lim_in_cod1 Rseq) . m) - it ).| < e;

 existence by a2, SEQ_2:def 6;

 uniqueness

 proof

 let z1,z2 be Real;

 assume that

 a4: for e st 0 < e holds ex M st for m st m >= M holds |.((( lim_in_cod1 Rseq) . m) - z1).| < e and

 a5: for e st 0 < e holds ex M st for m st m >= M holds |.((( lim_in_cod1 Rseq) . m) - z2).| < e;

 assume

 a6: z1 <> z2;

 set p = ( |.(z1 - z2).| / 2);



 a7: |.(z1 - z2).| > 0 by a6, COMPLEX1: 62;

 then

 consider M1 be Nat such that

 a8: for m st M1 <= m holds |.((( lim_in_cod1 Rseq) . m) - z1).| < p by a4;

 consider M2 be Nat such that

 a9: for m st M2 <= m holds |.((( lim_in_cod1 Rseq) . m) - z2).| < p by a5, a7;

 set M = ( max (M1,M2));



 a0: M is Nat by TARSKI: 1;

 for m st M <= m holds (2 * p) < (2 * p)

 proof

 let m;

 set s = ( lim_in_cod1 Rseq);

 assume

 a10: M <= m;

 M2 <= M by XXREAL_0: 25;

 then (M + M2) <= (M + m) by a10, XREAL_1: 7;

 then M2 <= m by XREAL_1: 6;

 then

 a11: |.((s . m) - z2).| < p by a9;

 |.(z1 - z2).| = |.((z1 - (s . m)) - (z2 - (s . m))).|;

 then |.(z1 - z2).| <= ( |.(z1 - (s . m)).| + |.(z2 - (s . m)).|) by COMPLEX1: 57;

 then

 a12: |.(z1 - z2).| <= ( |.((s . m) - z1).| + |.(z2 - (s . m)).|) by COMPLEX1: 60;

 M1 <= M by XXREAL_0: 25;

 then (M + M1) <= (M + m) by a10, XREAL_1: 7;

 then M1 <= m by XREAL_1: 6;

 then |.((s . m) - z1).| < p by a8;

 then ( |.((s . m) - z1).| + |.((s . m) - z2).|) < (p + p) by a11, XREAL_1: 8;

 hence thesis by a12, COMPLEX1: 60;

 end;

 hence contradiction by a0;

 end;

 end

 definition

 let Rseq;

 assume

 a2: ( lim_in_cod2 Rseq) is convergent;

 :: DBLSEQ_1:def8

 func cod2_major_iterated_lim Rseq -> Real means

 : def35: for e be Real st 0 < e holds ex N be Nat st for n be Nat st n >= N holds |.((( lim_in_cod2 Rseq) . n) - it ).| < e;

 existence by a2, SEQ_2:def 6;

 uniqueness

 proof

 let z1,z2 be Real;

 assume that

 a4: for e st 0 < e holds ex M st for m st m >= M holds |.((( lim_in_cod2 Rseq) . m) - z1).| < e and

 a5: for e st 0 < e holds ex M st for m st m >= M holds |.((( lim_in_cod2 Rseq) . m) - z2).| < e;

 assume

 a6: z1 <> z2;

 set p = ( |.(z1 - z2).| / 2);



 a7: |.(z1 - z2).| > 0 by a6, COMPLEX1: 62;

 then

 consider M1 be Nat such that

 a8: for m st M1 <= m holds |.((( lim_in_cod2 Rseq) . m) - z1).| < p by a4;

 consider M2 be Nat such that

 a9: for m st M2 <= m holds |.((( lim_in_cod2 Rseq) . m) - z2).| < p by a5, a7;

 set M = ( max (M1,M2));



 a0: M is Nat by TARSKI: 1;

 for m st M <= m holds (2 * p) < (2 * p)

 proof

 let m;

 set s = ( lim_in_cod2 Rseq);

 assume

 a10: M <= m;

 M2 <= M by XXREAL_0: 25;

 then (M + M2) <= (M + m) by a10, XREAL_1: 7;

 then M2 <= m by XREAL_1: 6;

 then

 a11: |.((s . m) - z2).| < p by a9;

 |.(z1 - z2).| = |.((z1 - (s . m)) - (z2 - (s . m))).|;

 then |.(z1 - z2).| <= ( |.(z1 - (s . m)).| + |.(z2 - (s . m)).|) by COMPLEX1: 57;

 then

 a12: |.(z1 - z2).| <= ( |.((s . m) - z1).| + |.(z2 - (s . m)).|) by COMPLEX1: 60;

 M1 <= M by XXREAL_0: 25;

 then (M + M1) <= (M + m) by a10, XREAL_1: 7;

 then M1 <= m by XREAL_1: 6;

 then |.((s . m) - z1).| < p by a8;

 then ( |.((s . m) - z1).| + |.((s . m) - z2).|) < (p + p) by a11, XREAL_1: 8;

 hence thesis by a12, COMPLEX1: 60;

 end;

 hence contradiction by a0;

 end;

 end

 definition

 let Rseq be Function of [: NAT , NAT :], REAL ;

 :: DBLSEQ_1:def9

 attr Rseq is uniformly_convergent_in_cod1 means Rseq is convergent_in_cod1 & for e be Real st e > 0 holds ex M be Nat st for m be Nat st m >= M holds for n be Nat holds |.((Rseq . (n,m)) - (( lim_in_cod1 Rseq) . n)).| < e;

 end

 definition

 let Rseq be Function of [: NAT , NAT :], REAL ;

 :: DBLSEQ_1:def10

 attr Rseq is uniformly_convergent_in_cod2 means Rseq is convergent_in_cod2 & for e be Real st e > 0 holds ex N be Nat st for n be Nat st n >= N holds for m be Nat holds |.((Rseq . (n,m)) - (( lim_in_cod2 Rseq) . m)).| < e;

 end

 definition

 let Rseq;

 :: DBLSEQ_1:def11

 attr Rseq is non-decreasing means for n1,m1,n2,m2 be Nat st n1 >= n2 & m1 >= m2 holds (Rseq . (n1,m1)) >= (Rseq . (n2,m2));

 :: DBLSEQ_1:def12

 attr Rseq is non-increasing means for n1,m1,n2,m2 be Nat st n1 >= n2 & m1 >= m2 holds (Rseq . (n1,m1)) <= (Rseq . (n2,m2));

 end

 theorem :: DBLSEQ_1:1



 th28: for a,b,c be Real st a <= b & b <= c holds |.b.| <= |.a.| or |.b.| <= |.c.|

 proof

 let a,b,c be Real;

 assume

 a1: a <= b & b <= c;

 per cases ;

 suppose b >= 0 ;

 then |.b.| = b & |.c.| = c by a1, ABSVALUE:def 1;

 hence thesis by a1;

 end;

 suppose b < 0 ;

 then |.a.| = ( - a) & |.b.| = ( - b) by a1, ABSVALUE:def 1;

 hence thesis by a1, XREAL_1: 24;

 end;

 end;

 registration

 cluster non-decreasing P-convergent -> bounded_below bounded_above for Function of [: NAT , NAT :], REAL ;

 coherence

 proof

 let Rseq be Function of [: NAT , NAT :], REAL ;

 assume

 a1: Rseq is non-decreasing P-convergent;

 then

 consider p be Real such that

 a3: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - p).| < e;

 consider N such that

 a4: for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - p).| < 1 by a3;



 a5: for n, m st n >= N & m >= N holds |.(Rseq . (n,m)).| < (1 + |.p.|)

 proof

 let n, m;

 assume n >= N & m >= N;

 then

 a6: |.((Rseq . (n,m)) - p).| < 1 by a4;

 |.((Rseq . (n,m)) - p).| >= ( |.(Rseq . (n,m)).| - |.p.|) by COMPLEX1: 59;

 then ( |.(Rseq . (n,m)).| - |.p.|) < 1 by a6, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| < (1 + |.p.|) by XREAL_1: 19;

 end;

 deffunc F( Element of NAT ) = $1;

 deffunc F1( Nat) = |.(Rseq . (1,$1)).|;

 reconsider E2 = { F(m) where m be Element of NAT : m <= N } as finite non empty Subset of NAT from ASYMPT_0:sch 2;

 reconsider EE = [:E2, E2:] as finite set;



 c1: E2 is finite;

 deffunc F( Element of NAT , Element of NAT ) = |.(Rseq . ($1,$2)).|;



 a9: { F(m,n) where m be Element of NAT , n be Element of NAT : m in E2 & n in E2 } is finite from FRAENKEL:sch 22( c1, c1);

 set F = { F(m,n) where m be Element of NAT , n be Element of NAT : m in E2 & n in E2 };

 N is Element of NAT by ORDINAL1:def 12;

 then N in E2;

 then

 b1: |.(Rseq . (N,N)).| in F;

 now

 let x be object;

 assume x in F;

 then

 consider p be Element of NAT , q be Element of NAT such that

 a10: x = F(p,q) & p in E2 & q in E2;

 thus x is real by a10;

 end;

 then

 reconsider F as non empty real-membered set by b1, MEMBERED:def 3;

 reconsider M1 = ( sup F) as Element of REAL by a9, XXREAL_2: 16;

 set M = ( max (M1,(1 + |.p.|)));



 a14: M >= (1 + |.p.|) & (1 + |.p.|) >= 1 & M >= M1 & M >= M1 by XXREAL_0: 25, XREAL_1: 31, COMPLEX1: 46;



 c1: for n, m holds |.(Rseq . (n,m)).| <= M

 proof

 let n, m;



 c0: n is Element of NAT & m is Element of NAT & N is Element of NAT by ORDINAL1:def 12;

 per cases ;

 suppose n >= N & m >= N;

 then |.(Rseq . (n,m)).| < (1 + |.p.|) by a5;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 suppose n < N & m < N;

 then n in E2 & m in E2 by c0;

 then |.(Rseq . (n,m)).| in F;

 then

 a15: |.(Rseq . (n,m)).| <= M1 by XXREAL_2: 4;

 M >= M1 by XXREAL_0: 25;

 hence |.(Rseq . (n,m)).| <= M by a15, XXREAL_0: 2;

 end;

 suppose

 a18: n < N & m >= N;

 then

 a19: (Rseq . (n,N)) <= (Rseq . (n,m)) & (Rseq . (n,m)) <= (Rseq . (N,m)) by a1;

 n in E2 & N in E2 by a18, c0;

 then |.(Rseq . (n,N)).| in F;

 then

 a20: |.(Rseq . (n,N)).| <= M1 by XXREAL_2: 4;



 a21: |.(Rseq . (N,m)).| < (1 + |.p.|) by a5, a18;

 per cases by a19, th28;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (n,N)).|;

 then |.(Rseq . (n,m)).| <= M1 by a20, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (N,m)).|;

 then |.(Rseq . (n,m)).| <= (1 + |.p.|) by a21, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 end;

 suppose

 a22: n >= N & m < N;

 then

 a23: (Rseq . (N,m)) <= (Rseq . (n,m)) & (Rseq . (n,m)) <= (Rseq . (n,N)) by a1;

 N in E2 & m in E2 by a22, c0;

 then |.(Rseq . (N,m)).| in F;

 then

 a24: |.(Rseq . (N,m)).| <= M1 by XXREAL_2: 4;



 a25: |.(Rseq . (n,N)).| < (1 + |.p.|) by a5, a22;

 per cases by a23, th28;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (N,m)).|;

 then |.(Rseq . (n,m)).| <= M1 by a24, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (n,N)).|;

 then |.(Rseq . (n,m)).| <= (1 + |.p.|) by a25, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 end;

 end;

 now

 let a be ExtReal;

 assume a in (Rseq .: [: NAT , NAT :]);

 then

 consider x be Element of [: NAT , NAT qua non empty set:] such that

 b2: x in [: NAT , NAT :] & a = (Rseq . x) by FUNCT_2: 65;

 consider n,m be object such that

 b3: n in NAT & m in NAT & x = [n, m] by ZFMISC_1:def 2;

 reconsider n, m as Element of NAT by b3;

 |.(Rseq . (n,m)).| <= M by c1;

 hence ( - M) <= a & a <= M by b2, b3, ABSVALUE: 5;

 end;

 then (for a be ExtReal st a in (Rseq .: [: NAT , NAT :]) holds ( - M) <= a) & (for a be ExtReal st a in (Rseq .: [: NAT , NAT :]) holds a <= M);

 then ( - M) is LowerBound of (Rseq .: [: NAT , NAT :]) & M is UpperBound of (Rseq .: [: NAT , NAT :]) by XXREAL_2:def 1, XXREAL_2:def 2;

 hence thesis by XXREAL_2:def 9, XXREAL_2:def 10;

 end;

 end

 registration

 cluster non-increasing P-convergent -> bounded_below bounded_above for Function of [: NAT , NAT :], REAL ;

 coherence

 proof

 let Rseq be Function of [: NAT , NAT :], REAL ;

 assume

 a1: Rseq is non-increasing P-convergent;

 then

 consider p be Real such that

 a3: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - p).| < e;

 consider N such that

 a4: for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - p).| < 1 by a3;



 a5: for n, m st n >= N & m >= N holds |.(Rseq . (n,m)).| < (1 + |.p.|)

 proof

 let n, m;

 assume n >= N & m >= N;

 then

 a6: |.((Rseq . (n,m)) - p).| < 1 by a4;

 |.((Rseq . (n,m)) - p).| >= ( |.(Rseq . (n,m)).| - |.p.|) by COMPLEX1: 59;

 then ( |.(Rseq . (n,m)).| - |.p.|) < 1 by a6, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| < (1 + |.p.|) by XREAL_1: 19;

 end;

 deffunc F1( Element of NAT ) = |.(Rseq . (1,$1)).|;

 deffunc F( Element of NAT ) = $1;

 reconsider E2 = { F(m) where m be Element of NAT : m <= N } as finite non empty Subset of NAT from ASYMPT_0:sch 2;

 reconsider EE = [:E2, E2:] as finite set;



 c1: E2 is finite;

 deffunc F( Element of NAT , Element of NAT ) = |.(Rseq . ($1,$2)).|;



 a9: { F(m,n) where m be Element of NAT , n be Element of NAT : m in E2 & n in E2 } is finite from FRAENKEL:sch 22( c1, c1);

 set F = { F(m,n) where m be Element of NAT , n be Element of NAT : m in E2 & n in E2 };

 N is Element of NAT by ORDINAL1:def 12;

 then N in E2;

 then

 b1: |.(Rseq . (N,N)).| in F;

 now

 let x be object;

 assume x in F;

 then

 consider p be Element of NAT , q be Element of NAT such that

 a10: x = F(p,q) & p in E2 & q in E2;

 thus x is real by a10;

 end;

 then

 reconsider F as non empty real-membered set by b1, MEMBERED:def 3;

 reconsider M1 = ( sup F) as Element of REAL by a9, XXREAL_2: 16;

 set M = ( max (M1,(1 + |.p.|)));



 a14: M >= (1 + |.p.|) & (1 + |.p.|) >= 1 & M >= M1 & M >= M1 by XXREAL_0: 25, XREAL_1: 31, COMPLEX1: 46;



 c1: for n, m holds |.(Rseq . (n,m)).| <= M

 proof

 let n, m;



 c0: n is Element of NAT & m is Element of NAT & N is Element of NAT by ORDINAL1:def 12;

 per cases ;

 suppose n >= N & m >= N;

 then |.(Rseq . (n,m)).| < (1 + |.p.|) by a5;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 suppose n < N & m < N;

 then n in E2 & m in E2 by c0;

 then |.(Rseq . (n,m)).| in F;

 then

 a15: |.(Rseq . (n,m)).| <= M1 by XXREAL_2: 4;

 M >= M1 by XXREAL_0: 25;

 hence |.(Rseq . (n,m)).| <= M by a15, XXREAL_0: 2;

 end;

 suppose

 a18: n < N & m >= N;

 then

 a19: (Rseq . (n,N)) >= (Rseq . (n,m)) & (Rseq . (n,m)) >= (Rseq . (N,m)) by a1;

 n in E2 & N in E2 by a18, c0;

 then |.(Rseq . (n,N)).| in F;

 then

 a20: |.(Rseq . (n,N)).| <= M1 by XXREAL_2: 4;



 a21: |.(Rseq . (N,m)).| < (1 + |.p.|) by a5, a18;

 per cases by a19, th28;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (n,N)).|;

 then |.(Rseq . (n,m)).| <= M1 by a20, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (N,m)).|;

 then |.(Rseq . (n,m)).| <= (1 + |.p.|) by a21, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 end;

 suppose

 a22: n >= N & m < N;

 then

 a23: (Rseq . (N,m)) >= (Rseq . (n,m)) & (Rseq . (n,m)) >= (Rseq . (n,N)) by a1;

 N in E2 & m in E2 by a22, c0;

 then |.(Rseq . (N,m)).| in F;

 then

 a24: |.(Rseq . (N,m)).| <= M1 by XXREAL_2: 4;



 a25: |.(Rseq . (n,N)).| < (1 + |.p.|) by a5, a22;

 per cases by a23, th28;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (N,m)).|;

 then |.(Rseq . (n,m)).| <= M1 by a24, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 suppose |.(Rseq . (n,m)).| <= |.(Rseq . (n,N)).|;

 then |.(Rseq . (n,m)).| <= (1 + |.p.|) by a25, XXREAL_0: 2;

 hence |.(Rseq . (n,m)).| <= M by a14, XXREAL_0: 2;

 end;

 end;

 end;

 now

 let a be ExtReal;

 assume a in (Rseq .: [: NAT , NAT :]);

 then

 consider x be Element of [: NAT , NAT :] such that

 b2: x in [: NAT , NAT :] & a = (Rseq . x) by FUNCT_2: 65;

 consider n,m be object such that

 b3: n in NAT & m in NAT & x = [n, m] by ZFMISC_1:def 2;

 reconsider n, m as Element of NAT by b3;

 |.(Rseq . (n,m)).| <= M by c1;

 hence ( - M) <= a & a <= M by b3, b2, ABSVALUE: 5;

 end;

 then (for a be ExtReal st a in (Rseq .: [: NAT , NAT :]) holds ( - M) <= a) & (for a be ExtReal st a in (Rseq .: [: NAT , NAT :]) holds a <= M);

 then ( - M) is LowerBound of (Rseq .: [: NAT , NAT :]) & M is UpperBound of (Rseq .: [: NAT , NAT :]) by XXREAL_2:def 1, XXREAL_2:def 2;

 hence thesis by XXREAL_2:def 9, XXREAL_2:def 10;

 end;

 end



 LM111: for r be Element of REAL holds ( [: NAT , NAT :] --> r) is P-convergent & ( [: NAT , NAT :] --> r) is convergent_in_cod1 & ( [: NAT , NAT :] --> r) is convergent_in_cod2

 proof

 let r be Element of REAL ;

 set Rseq = ( [: NAT , NAT :] --> r);



 a1: for n,m be Nat holds (Rseq . (n,m)) = r

 proof

 let n,m be Nat;

 n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;

 hence (Rseq . (n,m)) = r by FUNCOP_1: 70;

 end;

 a3:

 now

 let e be Real;

 assume

 a2: 0 < e;

 a4:

 now

 let n, m such that n >= 0 & m >= 0 ;

 (Rseq . (n,m)) = r by a1;

 hence |.((Rseq . (n,m)) - r).| < e by a2, COMPLEX1: 44;

 end;

 reconsider N = 0 as Nat;

 take N;

 thus for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - r).| < e by a4;

 end;

 b1:

 now

 let m be Element of NAT ;

 now

 let e be Real;

 assume

 b3: 0 < e;

 now

 let n be Nat;

 assume 0 <= n;



 b4: n is Element of NAT by ORDINAL1:def 12;

 then (( ProjMap2 (Rseq,m)) . n) = (Rseq . (n,m)) by MESFUNC9:def 7;

 then (( ProjMap2 (Rseq,m)) . n) = r by b4, FUNCOP_1: 70;

 hence |.((( ProjMap2 (Rseq,m)) . n) - r).| < e by b3, ABSVALUE: 2;

 end;

 hence ex N be Nat st for n be Nat st N <= n holds |.((( ProjMap2 (Rseq,m)) . n) - r).| < e;

 end;

 hence ( ProjMap2 (Rseq,m)) is convergent by SEQ_2:def 6;

 end;

 now

 let n be Element of NAT ;

 now

 let e be Real;

 assume

 c3: 0 < e;

 now

 let m be Nat;

 assume 0 <= m;



 c4: m is Element of NAT by ORDINAL1:def 12;

 then (( ProjMap1 (Rseq,n)) . m) = (Rseq . (n,m)) by MESFUNC9:def 6;

 then (( ProjMap1 (Rseq,n)) . m) = r by c4, FUNCOP_1: 70;

 hence |.((( ProjMap1 (Rseq,n)) . m) - r).| < e by c3, ABSVALUE: 2;

 end;

 hence ex M be Nat st for m be Nat st M <= m holds |.((( ProjMap1 (Rseq,n)) . m) - r).| < e;

 end;

 hence ( ProjMap1 (Rseq,n)) is convergent by SEQ_2:def 6;

 end;

 hence thesis by a3, b1;

 end;

 registration

 let r be Element of REAL ;

 cluster ( [: NAT , NAT :] --> r) -> P-convergent convergent_in_cod1 convergent_in_cod2;

 coherence by LM111;

 end

 theorem :: DBLSEQ_1:2

 for r be Element of REAL holds ( P-lim ( [: NAT , NAT :] --> r)) = r

 proof

 let r be Element of REAL ;

 set Rseq = ( [: NAT , NAT :] --> r);



 a1: for n,m be Nat holds (Rseq . (n,m)) = r

 proof

 let n,m be Nat;

 n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;

 hence (Rseq . (n,m)) = r by FUNCOP_1: 70;

 end;

 now

 let e be Real;

 assume

 a2: 0 < e;

 a4:

 now

 let n, m such that n >= 0 & m >= 0 ;

 (Rseq . (n,m)) = r by a1;

 hence |.((Rseq . (n,m)) - r).| < e by a2, COMPLEX1: 44;

 end;

 reconsider N = 0 as Nat;

 take N;

 thus for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - r).| < e by a4;

 end;

 hence ( P-lim ( [: NAT , NAT :] --> r)) = r by def6;

 end;

 registration

 cluster P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [: NAT , NAT :], REAL ;

 existence

 proof



 a1: 1 is Element of REAL by XREAL_0:def 1;

 then

 reconsider f = ( [: NAT , NAT :] --> 1) as Function of [: NAT , NAT :], REAL by FUNCOP_1: 46;

 f is P-convergent convergent_in_cod1 convergent_in_cod2 by a1;

 hence thesis;

 end;

 end

 reserve Pseq for P-convergent Function of [: NAT , NAT :], REAL ;

 registration

 let Pseq2 be P-convergent convergent_in_cod2 Function of [: NAT , NAT :], REAL ;

 cluster ( lim_in_cod2 Pseq2) -> convergent;

 coherence

 proof

 Pseq2 is P-convergent;

 then

 consider z be Real such that

 a3: for e st 0 < e holds ex N1 be Nat st for n, m st n >= N1 & m >= N1 holds |.((Pseq2 . (n,m)) - z).| < e;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod2 Pseq2) . n) - z).| < e

 proof

 let e;

 assume

 a8: 0 < e;

 then

 consider N1 be Nat such that

 a15: for n, m st n >= N1 & m >= N1 holds |.((Pseq2 . (n,m)) - z).| < (e / 2) by a3;



 a12: for n be Element of NAT st n >= N1 holds ex N2 be Nat st for m st m >= N2 holds |.((( ProjMap1 (Pseq2,n)) . m) - (( lim_in_cod2 Pseq2) . n)).| < (e / 2)

 proof

 let n be Element of NAT ;

 assume n >= N1;

 Pseq2 is convergent_in_cod2;

 then ( ProjMap1 (Pseq2,n)) is convergent;

 then

 consider N2 be Nat such that

 a9: for m be Nat st m >= N2 holds |.((( ProjMap1 (Pseq2,n)) . m) - ( lim ( ProjMap1 (Pseq2,n)))).| < (e / 2) by a8, SEQ_2:def 7;

 take N2;

 thus for m st m >= N2 holds |.((( ProjMap1 (Pseq2,n)) . m) - (( lim_in_cod2 Pseq2) . n)).| < (e / 2)

 proof

 let m;

 assume m >= N2;

 then |.((( ProjMap1 (Pseq2,n)) . m) - ( lim ( ProjMap1 (Pseq2,n)))).| < (e / 2) by a9;

 hence thesis by def33;

 end;

 end;

 take N1;

 thus for n st n >= N1 holds |.((( lim_in_cod2 Pseq2) . n) - z).| < e

 proof

 let n;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

 assume

 a14: n >= N1;

 then

 consider N2 be Nat such that

 a13: for m st m >= N2 holds |.((( ProjMap1 (Pseq2,n1)) . m) - (( lim_in_cod2 Pseq2) . n1)).| < (e / 2) by a12;

 reconsider M = ( max (N2,N1)) as Element of NAT by ORDINAL1:def 12;



 a17: (( ProjMap1 (Pseq2,n1)) . M) = (Pseq2 . (n,M)) by MESFUNC9:def 6;



 a16: M >= N2 & M >= N1 by XXREAL_0: 25;



 a18: |.((( lim_in_cod2 Pseq2) . n) - z).| <= ( |.((( lim_in_cod2 Pseq2) . n) - (( ProjMap1 (Pseq2,n1)) . M)).| + |.((Pseq2 . (n,M)) - z).|) by a17, COMPLEX1: 63;

 |.((( lim_in_cod2 Pseq2) . n) - (( ProjMap1 (Pseq2,n1)) . M)).| = |.((( ProjMap1 (Pseq2,n1)) . M) - (( lim_in_cod2 Pseq2) . n)).| by COMPLEX1: 60;

 then

 a20: |.((( lim_in_cod2 Pseq2) . n) - (( ProjMap1 (Pseq2,n1)) . M)).| < (e / 2) by a13, XXREAL_0: 25;

 |.((Pseq2 . (n1,M)) - z).| < (e / 2) by a15, a16, a14;

 then ( |.((( lim_in_cod2 Pseq2) . n) - (( ProjMap1 (Pseq2,n1)) . M)).| + |.((Pseq2 . (n,M)) - z).|) < ((e / 2) + (e / 2)) by a20, XREAL_1: 8;

 hence |.((( lim_in_cod2 Pseq2) . n) - z).| < e by a18, XXREAL_0: 2;

 end;

 end;

 hence ( lim_in_cod2 Pseq2) is convergent by SEQ_2:def 6;

 end;

 end

 theorem :: DBLSEQ_1:3

 Rseq is P-convergent convergent_in_cod2 implies ( P-lim Rseq) = ( cod2_major_iterated_lim Rseq)

 proof

 assume

 a1: Rseq is P-convergent convergent_in_cod2;

 then

 consider z be Real such that

 a3: for e st 0 < e holds ex N1 be Nat st for n, m st n >= N1 & m >= N1 holds |.((Rseq . (n,m)) - z).| < e;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod2 Rseq) . n) - z).| < e

 proof

 let e;

 assume

 a8: 0 < e;

 then

 consider N1 be Nat such that

 a15: for n, m st n >= N1 & m >= N1 holds |.((Rseq . (n,m)) - z).| < (e / 2) by a3;



 a12: for n be Element of NAT st n >= N1 holds ex N2 be Nat st for m st m >= N2 holds |.((( ProjMap1 (Rseq,n)) . m) - (( lim_in_cod2 Rseq) . n)).| < (e / 2)

 proof

 let n be Element of NAT ;

 assume n >= N1;

 ( ProjMap1 (Rseq,n)) is convergent by a1;

 then

 consider N2 be Nat such that

 a9: for m be Nat st m >= N2 holds |.((( ProjMap1 (Rseq,n)) . m) - ( lim ( ProjMap1 (Rseq,n)))).| < (e / 2) by a8, SEQ_2:def 7;

 take N2;

 thus for m st m >= N2 holds |.((( ProjMap1 (Rseq,n)) . m) - (( lim_in_cod2 Rseq) . n)).| < (e / 2)

 proof

 let m;

 assume m >= N2;

 then |.((( ProjMap1 (Rseq,n)) . m) - ( lim ( ProjMap1 (Rseq,n)))).| < (e / 2) by a9;

 hence thesis by def33;

 end;

 end;

 take N1;

 thus for n st n >= N1 holds |.((( lim_in_cod2 Rseq) . n) - z).| < e

 proof

 let n;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

 assume

 a14: n >= N1;

 then

 consider N2 be Nat such that

 a13: for m st m >= N2 holds |.((( ProjMap1 (Rseq,n1)) . m) - (( lim_in_cod2 Rseq) . n1)).| < (e / 2) by a12;

 reconsider M = ( max (N2,N1)) as Element of NAT by ORDINAL1:def 12;



 a17: (( ProjMap1 (Rseq,n1)) . M) = (Rseq . (n,M)) by MESFUNC9:def 6;



 a16: M >= N2 & M >= N1 by XXREAL_0: 25;



 a18: |.((( lim_in_cod2 Rseq) . n) - z).| <= ( |.((( lim_in_cod2 Rseq) . n) - (( ProjMap1 (Rseq,n1)) . M)).| + |.((Rseq . (n,M)) - z).|) by a17, COMPLEX1: 63;

 |.((( lim_in_cod2 Rseq) . n) - (( ProjMap1 (Rseq,n1)) . M)).| = |.((( ProjMap1 (Rseq,n1)) . M) - (( lim_in_cod2 Rseq) . n)).| by COMPLEX1: 60;

 then

 a20: |.((( lim_in_cod2 Rseq) . n) - (( ProjMap1 (Rseq,n1)) . M)).| < (e / 2) by a13, XXREAL_0: 25;

 |.((Rseq . (n1,M)) - z).| < (e / 2) by a15, a16, a14;

 then ( |.((( lim_in_cod2 Rseq) . n) - (( ProjMap1 (Rseq,n1)) . M)).| + |.((Rseq . (n,M)) - z).|) < ((e / 2) + (e / 2)) by a20, XREAL_1: 8;

 hence |.((( lim_in_cod2 Rseq) . n) - z).| < e by a18, XXREAL_0: 2;

 end;

 end;

 then

 a21: ( lim_in_cod2 Rseq) is convergent by SEQ_2:def 6;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod2 Rseq) . n) - ( P-lim Rseq)).| < e

 proof

 let e;

 assume

 a22: 0 < e;

 then

 consider N1 be Nat such that

 a23: for n, m st n >= N1 & m >= N1 holds |.((Rseq . (n,m)) - ( P-lim Rseq)).| < (e / 2) by a1, def6;

 take N = N1;

 hereby

 let n;

 assume n >= N;

 then

 a27: for m st m >= N1 holds |.((Rseq . (n,m)) - ( P-lim Rseq)).| < (e / 2) by a23;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

 ( ProjMap1 (Rseq,n1)) is convergent by a1;

 then

 consider N3 be Nat such that

 a29: for m st m >= N3 holds |.((( ProjMap1 (Rseq,n1)) . m) - ( lim ( ProjMap1 (Rseq,n1)))).| < (e / 2) by a22, SEQ_2:def 7;

 reconsider M = ( max (N1,N3)) as Element of NAT by ORDINAL1:def 12;



 a31: |.((Rseq . (n,M)) - ( P-lim Rseq)).| < (e / 2) by a27, XXREAL_0: 25;

 (( ProjMap1 (Rseq,n1)) . M) = (Rseq . (n,M)) by MESFUNC9:def 6;

 then |.((Rseq . (n,M)) - ( lim ( ProjMap1 (Rseq,n1)))).| < (e / 2) by a29, XXREAL_0: 25;

 then |.((Rseq . (n,M)) - (( lim_in_cod2 Rseq) . n)).| < (e / 2) by def33;

 then |.((( lim_in_cod2 Rseq) . n) - (Rseq . (n,M))).| < (e / 2) by COMPLEX1: 60;

 then

 a32: ( |.((( lim_in_cod2 Rseq) . n) - (Rseq . (n,M))).| + |.((Rseq . (n,M)) - ( P-lim Rseq)).|) < ((e / 2) + (e / 2)) by a31, XREAL_1: 8;

 |.((( lim_in_cod2 Rseq) . n) - ( P-lim Rseq)).| <= ( |.((( lim_in_cod2 Rseq) . n) - (Rseq . (n,M))).| + |.((Rseq . (n,M)) - ( P-lim Rseq)).|) by COMPLEX1: 63;

 hence |.((( lim_in_cod2 Rseq) . n) - ( P-lim Rseq)).| < e by a32, XXREAL_0: 2;

 end;

 end;

 hence thesis by a21, def35;

 end;

 registration

 let Pseq1 be P-convergent convergent_in_cod1 Function of [: NAT , NAT :], REAL ;

 cluster ( lim_in_cod1 Pseq1) -> convergent;

 coherence

 proof

 Pseq1 is P-convergent;

 then

 consider z be Real such that

 a3: for e st 0 < e holds ex N1 be Nat st for n, m st n >= N1 & m >= N1 holds |.((Pseq1 . (n,m)) - z).| < e;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod1 Pseq1) . n) - z).| < e

 proof

 let e;

 assume

 a8: 0 < e;

 then

 consider N1 be Nat such that

 a15: for n, m st n >= N1 & m >= N1 holds |.((Pseq1 . (n,m)) - z).| < (e / 2) by a3;



 a12: for n be Element of NAT st n >= N1 holds ex N2 be Nat st for m st m >= N2 holds |.((( ProjMap2 (Pseq1,n)) . m) - (( lim_in_cod1 Pseq1) . n)).| < (e / 2)

 proof

 let n be Element of NAT ;

 assume n >= N1;

 Pseq1 is convergent_in_cod1;

 then ( ProjMap2 (Pseq1,n)) is convergent;

 then

 consider N2 be Nat such that

 a9: for m st m >= N2 holds |.((( ProjMap2 (Pseq1,n)) . m) - ( lim ( ProjMap2 (Pseq1,n)))).| < (e / 2) by a8, SEQ_2:def 7;

 take N2;

 thus for m st m >= N2 holds |.((( ProjMap2 (Pseq1,n)) . m) - (( lim_in_cod1 Pseq1) . n)).| < (e / 2)

 proof

 let m;

 assume m >= N2;

 then |.((( ProjMap2 (Pseq1,n)) . m) - ( lim ( ProjMap2 (Pseq1,n)))).| < (e / 2) by a9;

 hence thesis by def32;

 end;

 end;

 take N1;

 thus for n st n >= N1 holds |.((( lim_in_cod1 Pseq1) . n) - z).| < e

 proof

 let n be Nat;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

 assume

 a14: n >= N1;

 then

 consider N2 be Nat such that

 a13: for m st m >= N2 holds |.((( ProjMap2 (Pseq1,n1)) . m) - (( lim_in_cod1 Pseq1) . n)).| < (e / 2) by a12;

 reconsider M = ( max (N2,N1)) as Element of NAT by ORDINAL1:def 12;



 a17: (( ProjMap2 (Pseq1,n1)) . M) = (Pseq1 . (M,n)) by MESFUNC9:def 7;



 a16: M >= N2 & M >= N1 by XXREAL_0: 25;



 a18: |.((( lim_in_cod1 Pseq1) . n) - z).| <= ( |.((( lim_in_cod1 Pseq1) . n) - (( ProjMap2 (Pseq1,n1)) . M)).| + |.((Pseq1 . (M,n)) - z).|) by a17, COMPLEX1: 63;

 |.((( lim_in_cod1 Pseq1) . n) - (( ProjMap2 (Pseq1,n1)) . M)).| = |.((( ProjMap2 (Pseq1,n1)) . M) - (( lim_in_cod1 Pseq1) . n)).| by COMPLEX1: 60;

 then

 a20: |.((( lim_in_cod1 Pseq1) . n) - (( ProjMap2 (Pseq1,n1)) . M)).| < (e / 2) by a13, XXREAL_0: 25;

 |.((Pseq1 . (M,n1)) - z).| < (e / 2) by a15, a16, a14;

 then ( |.((( lim_in_cod1 Pseq1) . n) - (( ProjMap2 (Pseq1,n1)) . M)).| + |.((Pseq1 . (M,n)) - z).|) < ((e / 2) + (e / 2)) by a20, XREAL_1: 8;

 hence |.((( lim_in_cod1 Pseq1) . n) - z).| < e by a18, XXREAL_0: 2;

 end;

 end;

 hence ( lim_in_cod1 Pseq1) is convergent by SEQ_2:def 6;

 end;

 end

 theorem :: DBLSEQ_1:4

 Rseq is P-convergent convergent_in_cod1 implies ( P-lim Rseq) = ( cod1_major_iterated_lim Rseq)

 proof

 assume

 a1: Rseq is P-convergent convergent_in_cod1;

 then

 consider z be Real such that

 a3: for e st 0 < e holds ex N1 be Nat st for n, m st n >= N1 & m >= N1 holds |.((Rseq . (n,m)) - z).| < e;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod1 Rseq) . n) - z).| < e

 proof

 let e;

 assume

 a8: 0 < e;

 then

 consider N1 be Nat such that

 a15: for n, m st n >= N1 & m >= N1 holds |.((Rseq . (n,m)) - z).| < (e / 2) by a3;



 a12: for n be Element of NAT st n >= N1 holds ex N2 be Nat st for m st m >= N2 holds |.((( ProjMap2 (Rseq,n)) . m) - (( lim_in_cod1 Rseq) . n)).| < (e / 2)

 proof

 let n be Element of NAT ;

 assume n >= N1;

 ( ProjMap2 (Rseq,n)) is convergent by a1;

 then

 consider N2 be Nat such that

 a9: for m st m >= N2 holds |.((( ProjMap2 (Rseq,n)) . m) - ( lim ( ProjMap2 (Rseq,n)))).| < (e / 2) by a8, SEQ_2:def 7;

 take N2;

 thus for m st m >= N2 holds |.((( ProjMap2 (Rseq,n)) . m) - (( lim_in_cod1 Rseq) . n)).| < (e / 2)

 proof

 let m;

 assume m >= N2;

 then |.((( ProjMap2 (Rseq,n)) . m) - ( lim ( ProjMap2 (Rseq,n)))).| < (e / 2) by a9;

 hence thesis by def32;

 end;

 end;

 take N1;

 thus for n st n >= N1 holds |.((( lim_in_cod1 Rseq) . n) - z).| < e

 proof

 let n be Nat;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

 assume

 a14: n >= N1;

 then

 consider N2 be Nat such that

 a13: for m st m >= N2 holds |.((( ProjMap2 (Rseq,n1)) . m) - (( lim_in_cod1 Rseq) . n)).| < (e / 2) by a12;

 reconsider M = ( max (N2,N1)) as Element of NAT by ORDINAL1:def 12;



 a17: (( ProjMap2 (Rseq,n1)) . M) = (Rseq . (M,n)) by MESFUNC9:def 7;



 a16: M >= N2 & M >= N1 by XXREAL_0: 25;



 a18: |.((( lim_in_cod1 Rseq) . n) - z).| <= ( |.((( lim_in_cod1 Rseq) . n) - (( ProjMap2 (Rseq,n1)) . M)).| + |.((Rseq . (M,n)) - z).|) by a17, COMPLEX1: 63;

 |.((( lim_in_cod1 Rseq) . n) - (( ProjMap2 (Rseq,n1)) . M)).| = |.((( ProjMap2 (Rseq,n1)) . M) - (( lim_in_cod1 Rseq) . n)).| by COMPLEX1: 60;

 then

 a20: |.((( lim_in_cod1 Rseq) . n) - (( ProjMap2 (Rseq,n1)) . M)).| < (e / 2) by a13, XXREAL_0: 25;

 |.((Rseq . (M,n1)) - z).| < (e / 2) by a15, a16, a14;

 then ( |.((( lim_in_cod1 Rseq) . n) - (( ProjMap2 (Rseq,n1)) . M)).| + |.((Rseq . (M,n)) - z).|) < ((e / 2) + (e / 2)) by a20, XREAL_1: 8;

 hence |.((( lim_in_cod1 Rseq) . n) - z).| < e by a18, XXREAL_0: 2;

 end;

 end;

 then

 a21: ( lim_in_cod1 Rseq) is convergent by SEQ_2:def 6;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod1 Rseq) . n) - ( P-lim Rseq)).| < e

 proof

 let e;

 assume

 a22: 0 < e;

 then

 consider N1 be Nat such that

 a23: for n, m st n >= N1 & m >= N1 holds |.((Rseq . (n,m)) - ( P-lim Rseq)).| < (e / 2) by a1, def6;

 take N = N1;

 hereby

 let n;

 assume n >= N;

 then

 a27: for m st m >= N1 holds |.((Rseq . (m,n)) - ( P-lim Rseq)).| < (e / 2) by a23;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

 ( ProjMap2 (Rseq,n1)) is convergent by a1;

 then

 consider N3 be Nat such that

 a29: for m st m >= N3 holds |.((( ProjMap2 (Rseq,n1)) . m) - ( lim ( ProjMap2 (Rseq,n1)))).| < (e / 2) by a22, SEQ_2:def 7;

 reconsider M = ( max (N1,N3)) as Element of NAT by ORDINAL1:def 12;



 a31: |.((Rseq . (M,n)) - ( P-lim Rseq)).| < (e / 2) by a27, XXREAL_0: 25;

 (( ProjMap2 (Rseq,n1)) . M) = (Rseq . (M,n)) by MESFUNC9:def 7;

 then |.((Rseq . (M,n)) - ( lim ( ProjMap2 (Rseq,n1)))).| < (e / 2) by a29, XXREAL_0: 25;

 then |.((Rseq . (M,n)) - (( lim_in_cod1 Rseq) . n)).| < (e / 2) by def32;

 then |.((( lim_in_cod1 Rseq) . n) - (Rseq . (M,n))).| < (e / 2) by COMPLEX1: 60;

 then

 a32: ( |.((( lim_in_cod1 Rseq) . n) - (Rseq . (M,n))).| + |.((Rseq . (M,n)) - ( P-lim Rseq)).|) < ((e / 2) + (e / 2)) by a31, XREAL_1: 8;

 |.((( lim_in_cod1 Rseq) . n) - ( P-lim Rseq)).| <= ( |.((( lim_in_cod1 Rseq) . n) - (Rseq . (M,n))).| + |.((Rseq . (M,n)) - ( P-lim Rseq)).|) by COMPLEX1: 63;

 hence |.((( lim_in_cod1 Rseq) . n) - ( P-lim Rseq)).| < e by a32, XXREAL_0: 2;

 end;

 end;

 hence thesis by a21, def34;

 end;



 LM112: Rseq is non-decreasing bounded_above implies Rseq is P-convergent convergent_in_cod1 convergent_in_cod2

 proof

 assume that

 a1: Rseq is non-decreasing and

 a2: Rseq is bounded_above;

 reconsider M = ( sup (Rseq .: [: NAT , NAT :])) as Element of REAL by a2, XXREAL_2: 16;



 b2: [: NAT , NAT :] = ( dom Rseq) by FUNCT_2:def 1;

 then

 b3: ( rng Rseq) = (Rseq .: [: NAT , NAT :]) by RELAT_1: 113;



 a3: for e st 0 < e holds ex N st (Rseq . (N,N)) > (M - e)

 proof

 let e;

 assume

 a4: 0 < e;

 assume

 a7: for n holds (Rseq . (n,n)) <= (M - e);

 now

 let a be ExtReal;

 assume a in (Rseq .: [: NAT , NAT :]);

 then

 consider x be object such that

 a5: x in ( dom Rseq) & a = (Rseq . x) by b3, FUNCT_1:def 3;

 consider i,j be object such that

 a6: i in NAT & j in NAT & x = [i, j] by a5, ZFMISC_1:def 2;

 reconsider i, j as Nat by a6;



 a0: ( max (i,j)) is Nat by TARSKI: 1;

 ( max (i,j)) >= i & ( max (i,j)) >= j by XXREAL_0: 25;

 then

 a8: (Rseq . (( max (i,j)),( max (i,j)))) >= (Rseq . (i,j)) by a1, a0;

 (Rseq . (( max (i,j)),( max (i,j)))) <= (M - e) by a7, a0;

 hence a <= (M - e) by a5, a6, a8, XXREAL_0: 2;

 end;

 then (M - e) is UpperBound of (Rseq .: [: NAT , NAT :]) by XXREAL_2:def 1;

 hence contradiction by a4, XREAL_1: 44, XXREAL_2:def 3;

 end;

 for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - M).| < e

 proof

 let e;

 assume

 a5: 0 < e;

 then

 consider N such that

 a10: (Rseq . (N,N)) > (M - e) by a3;

 take N;

 hereby

 let n, m;

 assume n >= N & m >= N;

 then

 a11: (Rseq . (N,N)) <= (Rseq . (n,m)) by a1;

 n in NAT & m in NAT by ORDINAL1:def 12;

 then [n, m] in [: NAT , NAT :] by ZFMISC_1:def 2;

 then

 a12: (Rseq . (n,m)) <= M by b2, b3, FUNCT_1: 3, XXREAL_2: 4;

 M < (M + e) by a5, XREAL_1: 29;

 then (M - e) < (Rseq . (n,m)) & (Rseq . (n,m)) < (M + e) by a10, a11, a12, XXREAL_0: 2;

 hence |.((Rseq . (n,m)) - M).| < e by RINFSUP1: 1;

 end;

 end;

 hence Rseq is P-convergent;

 for m be Element of NAT holds ( ProjMap2 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 NAT = ( dom ( ProjMap2 (Rseq,m))) by FUNCT_2:def 1;

 then

 c3: ( rng ( ProjMap2 (Rseq,m))) = (( ProjMap2 (Rseq,m)) .: NAT ) by RELAT_1: 113;

 now

 let a be object;

 assume a in (( ProjMap2 (Rseq,m)) .: NAT );

 then

 consider i be object such that

 c4: i in ( dom ( ProjMap2 (Rseq,m))) & a = (( ProjMap2 (Rseq,m)) . i) by c3, FUNCT_1:def 3;

 reconsider i as Element of NAT by c4;

 [i, m] in [: NAT , NAT :] by ZFMISC_1:def 2;

 then (Rseq . (i,m)) in (Rseq .: [: NAT , NAT :]) by b2, b3, FUNCT_1: 3;

 hence a in (Rseq .: [: NAT , NAT :]) by c4, MESFUNC9:def 7;

 end;

 then

 c5: ( ProjMap2 (Rseq,m)) is bounded_above by a2, XXREAL_2: 43, TARSKI:def 3;

 now

 let n;

 n is Element of NAT by ORDINAL1:def 12;

 then

 c6: (( ProjMap2 (Rseq,m)) . n) = (Rseq . (n,m)) & (( ProjMap2 (Rseq,m)) . (n + 1)) = (Rseq . ((n + 1),m)) by MESFUNC9:def 7;

 n <= (n + 1) by NAT_1: 11;

 hence (( ProjMap2 (Rseq,m)) . n) <= (( ProjMap2 (Rseq,m)) . (n + 1)) by a1, c6;

 end;

 then ( ProjMap2 (Rseq,m)) is non-decreasing by SEQM_3:def 8;

 hence ( ProjMap2 (Rseq,m)) is convergent by c5;

 end;

 hence Rseq is convergent_in_cod1;

 for m be Element of NAT holds ( ProjMap1 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 NAT = ( dom ( ProjMap1 (Rseq,m))) by FUNCT_2:def 1;

 then

 c3: ( rng ( ProjMap1 (Rseq,m))) = (( ProjMap1 (Rseq,m)) .: NAT ) by RELAT_1: 113;

 now

 let a be object;

 assume a in (( ProjMap1 (Rseq,m)) .: NAT );

 then

 consider i be object such that

 c4: i in ( dom ( ProjMap1 (Rseq,m))) & a = (( ProjMap1 (Rseq,m)) . i) by c3, FUNCT_1:def 3;

 reconsider i as Element of NAT by c4;

 [m, i] in [: NAT , NAT :] by ZFMISC_1:def 2;

 then (Rseq . (m,i)) in (Rseq .: [: NAT , NAT :]) by b2, b3, FUNCT_1: 3;

 hence a in (Rseq .: [: NAT , NAT :]) by c4, MESFUNC9:def 6;

 end;

 then

 c5: ( ProjMap1 (Rseq,m)) is bounded_above by a2, XXREAL_2: 43, TARSKI:def 3;

 now

 let n;

 n is Element of NAT by ORDINAL1:def 12;

 then

 c6: (( ProjMap1 (Rseq,m)) . n) = (Rseq . (m,n)) & (( ProjMap1 (Rseq,m)) . (n + 1)) = (Rseq . (m,(n + 1))) by MESFUNC9:def 6;

 n <= (n + 1) by NAT_1: 11;

 hence (( ProjMap1 (Rseq,m)) . n) <= (( ProjMap1 (Rseq,m)) . (n + 1)) by a1, c6;

 end;

 then ( ProjMap1 (Rseq,m)) is non-decreasing by SEQM_3:def 8;

 hence ( ProjMap1 (Rseq,m)) is convergent by c5;

 end;

 hence Rseq is convergent_in_cod2;

 end;

 registration

 cluster non-decreasing bounded_above -> P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [: NAT , NAT :], REAL ;

 coherence by LM112;

 end



 LM113: Rseq is non-increasing bounded_below implies Rseq is P-convergent convergent_in_cod1 convergent_in_cod2

 proof

 assume that

 a1: Rseq is non-increasing and

 a2: Rseq is bounded_below;

 reconsider M = ( inf (Rseq .: [: NAT , NAT :])) as Element of REAL by a2, XXREAL_2: 15;



 b2: [: NAT , NAT :] = ( dom Rseq) by FUNCT_2:def 1;

 then

 b3: ( rng Rseq) = (Rseq .: [: NAT , NAT :]) by RELAT_1: 113;



 a3: for e st 0 < e holds ex N st (Rseq . (N,N)) < (M + e)

 proof

 let e;

 assume

 a4: 0 < e;

 assume

 a7: for n holds (Rseq . (n,n)) >= (M + e);

 now

 let a be ExtReal;

 assume a in (Rseq .: [: NAT , NAT :]);

 then

 consider x be object such that

 a5: x in ( dom Rseq) & a = (Rseq . x) by b3, FUNCT_1:def 3;

 consider i,j be object such that

 a6: i in NAT & j in NAT & x = [i, j] by a5, ZFMISC_1:def 2;

 reconsider i, j as Nat by a6;



 a0: ( max (i,j)) is Nat by TARSKI: 1;

 ( max (i,j)) >= i & ( max (i,j)) >= j by XXREAL_0: 25;

 then

 a8: (Rseq . (( max (i,j)),( max (i,j)))) <= (Rseq . (i,j)) by a1, a0;

 (Rseq . (( max (i,j)),( max (i,j)))) >= (M + e) by a7, a0;

 hence a >= (M + e) by a5, a6, a8, XXREAL_0: 2;

 end;

 then (M + e) is LowerBound of (Rseq .: [: NAT , NAT :]) by XXREAL_2:def 2;

 hence contradiction by a4, XREAL_1: 29, XXREAL_2:def 4;

 end;

 for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - M).| < e

 proof

 let e;

 assume

 a5: 0 < e;

 then

 consider N such that

 a10: (Rseq . (N,N)) < (M + e) by a3;

 take N;

 hereby

 let n, m;

 assume n >= N & m >= N;

 then

 a11: (Rseq . (N,N)) >= (Rseq . (n,m)) by a1;

 n in NAT & m in NAT by ORDINAL1:def 12;

 then [n, m] in [: NAT , NAT :] by ZFMISC_1:def 2;

 then

 a12: (Rseq . (n,m)) >= M by b2, b3, FUNCT_1: 3, XXREAL_2: 3;

 M > (M - e) by a5, XREAL_1: 44;

 then (M - e) < (Rseq . (n,m)) & (Rseq . (n,m)) < (M + e) by a10, a11, a12, XXREAL_0: 2;

 hence |.((Rseq . (n,m)) - M).| < e by RINFSUP1: 1;

 end;

 end;

 hence Rseq is P-convergent;

 for m be Element of NAT holds ( ProjMap2 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 NAT = ( dom ( ProjMap2 (Rseq,m))) by FUNCT_2:def 1;

 then

 c3: ( rng ( ProjMap2 (Rseq,m))) = (( ProjMap2 (Rseq,m)) .: NAT ) by RELAT_1: 113;

 now

 let a be object;

 assume a in (( ProjMap2 (Rseq,m)) .: NAT );

 then

 consider i be object such that

 c4: i in ( dom ( ProjMap2 (Rseq,m))) & a = (( ProjMap2 (Rseq,m)) . i) by c3, FUNCT_1:def 3;

 reconsider i as Element of NAT by c4;

 [i, m] in [: NAT , NAT :] by ZFMISC_1:def 2;

 then (Rseq . (i,m)) in (Rseq .: [: NAT , NAT :]) by b2, b3, FUNCT_1: 3;

 hence a in (Rseq .: [: NAT , NAT :]) by c4, MESFUNC9:def 7;

 end;

 then

 c5: ( ProjMap2 (Rseq,m)) is bounded_below by a2, XXREAL_2: 44, TARSKI:def 3;

 now

 let n;

 n is Element of NAT by ORDINAL1:def 12;

 then

 c6: (( ProjMap2 (Rseq,m)) . n) = (Rseq . (n,m)) & (( ProjMap2 (Rseq,m)) . (n + 1)) = (Rseq . ((n + 1),m)) by MESFUNC9:def 7;

 n <= (n + 1) by NAT_1: 11;

 hence (( ProjMap2 (Rseq,m)) . n) >= (( ProjMap2 (Rseq,m)) . (n + 1)) by a1, c6;

 end;

 then ( ProjMap2 (Rseq,m)) is non-increasing by SEQM_3:def 9;

 hence ( ProjMap2 (Rseq,m)) is convergent by c5;

 end;

 hence Rseq is convergent_in_cod1;

 for m be Element of NAT holds ( ProjMap1 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 NAT = ( dom ( ProjMap1 (Rseq,m))) by FUNCT_2:def 1;

 then

 c3: ( rng ( ProjMap1 (Rseq,m))) = (( ProjMap1 (Rseq,m)) .: NAT ) by RELAT_1: 113;

 now

 let a be object;

 assume a in (( ProjMap1 (Rseq,m)) .: NAT );

 then

 consider i be object such that

 c4: i in ( dom ( ProjMap1 (Rseq,m))) & a = (( ProjMap1 (Rseq,m)) . i) by c3, FUNCT_1:def 3;

 reconsider i as Element of NAT by c4;

 [m, i] in [: NAT , NAT :] by ZFMISC_1:def 2;

 then (Rseq . (m,i)) in (Rseq .: [: NAT , NAT :]) by b2, b3, FUNCT_1: 3;

 hence a in (Rseq .: [: NAT , NAT :]) by c4, MESFUNC9:def 6;

 end;

 then

 c5: ( ProjMap1 (Rseq,m)) is bounded_below by a2, XXREAL_2: 44, TARSKI:def 3;

 now

 let n;

 n is Element of NAT by ORDINAL1:def 12;

 then

 c6: (( ProjMap1 (Rseq,m)) . n) = (Rseq . (m,n)) & (( ProjMap1 (Rseq,m)) . (n + 1)) = (Rseq . (m,(n + 1))) by MESFUNC9:def 6;

 n <= (n + 1) by NAT_1: 11;

 hence (( ProjMap1 (Rseq,m)) . n) >= (( ProjMap1 (Rseq,m)) . (n + 1)) by a1, c6;

 end;

 then ( ProjMap1 (Rseq,m)) is non-increasing by SEQM_3:def 9;

 hence ( ProjMap1 (Rseq,m)) is convergent by c5;

 end;

 hence Rseq is convergent_in_cod2;

 end;

 registration

 cluster non-increasing bounded_below -> P-convergent convergent_in_cod1 convergent_in_cod2 for Function of [: NAT , NAT :], REAL ;

 coherence by LM113;

 end

 theorem :: DBLSEQ_1:5

 Rseq is uniformly_convergent_in_cod1 & ( lim_in_cod1 Rseq) is convergent implies Rseq is P-convergent & ( P-lim Rseq) = ( cod1_major_iterated_lim Rseq)

 proof

 assume that

 a3: Rseq is uniformly_convergent_in_cod1 and

 a2: ( lim_in_cod1 Rseq) is convergent;

 a4:

 now

 let e be Real;

 assume

 a5: 0 < e;

 then

 consider N1 be Nat such that

 a6: for m st m >= N1 holds for n holds |.((Rseq . (n,m)) - (( lim_in_cod1 Rseq) . n)).| < (e / 2) by a3;

 consider z be Real such that

 a7: for e st e > 0 holds ex N2 be Nat st for m st m >= N2 holds |.((( lim_in_cod1 Rseq) . m) - z).| < e by a2, SEQ_2:def 6;



 a8: z = ( cod1_major_iterated_lim Rseq) by a2, a7, def34;

 consider N2 be Nat such that

 a9: for n st n >= N2 holds |.((( lim_in_cod1 Rseq) . n) - z).| < (e / 2) by a5, a7;

 set N = ( max (N1,N2));



 a0: N is Nat by TARSKI: 1;

 for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( cod1_major_iterated_lim Rseq)).| < e

 proof

 let n, m;

 assume

 a10: n >= N & m >= N;

 N >= N1 & N >= N2 by XXREAL_0: 25;

 then n >= N2 & m >= N1 by a10, XXREAL_0: 2;

 then |.((Rseq . (n,m)) - (( lim_in_cod1 Rseq) . n)).| < (e / 2) & |.((( lim_in_cod1 Rseq) . n) - z).| < (e / 2) by a6, a9;

 then

 a12: ( |.((Rseq . (n,m)) - (( lim_in_cod1 Rseq) . n)).| + |.((( lim_in_cod1 Rseq) . n) - z).|) < ((e / 2) + (e / 2)) by XREAL_1: 8;

 |.((Rseq . (n,m)) - ( cod1_major_iterated_lim Rseq)).| <= ( |.((Rseq . (n,m)) - (( lim_in_cod1 Rseq) . n)).| + |.((( lim_in_cod1 Rseq) . n) - ( cod1_major_iterated_lim Rseq)).|) by COMPLEX1: 63;

 hence |.((Rseq . (n,m)) - ( cod1_major_iterated_lim Rseq)).| < e by a8, a12, XXREAL_0: 2;

 end;

 hence ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( cod1_major_iterated_lim Rseq)).| < e by a0;

 end;

 hence Rseq is P-convergent;

 hence thesis by a4, def6;

 end;

 theorem :: DBLSEQ_1:6

 Rseq is uniformly_convergent_in_cod2 & ( lim_in_cod2 Rseq) is convergent implies Rseq is P-convergent & ( P-lim Rseq) = ( cod2_major_iterated_lim Rseq)

 proof

 assume that

 a3: Rseq is uniformly_convergent_in_cod2 and

 a2: ( lim_in_cod2 Rseq) is convergent;

 a4:

 now

 let e;

 assume

 a5: 0 < e;

 then

 consider N1 be Nat such that

 a6: for n st n >= N1 holds for m holds |.((Rseq . (n,m)) - (( lim_in_cod2 Rseq) . m)).| < (e / 2) by a3;

 consider z be Real such that

 a7: for e st e > 0 holds ex N2 be Nat st for n st n >= N2 holds |.((( lim_in_cod2 Rseq) . n) - z).| < e by a2, SEQ_2:def 6;



 a8: z = ( cod2_major_iterated_lim Rseq) by a2, a7, def35;

 consider N2 be Nat such that

 a9: for n st n >= N2 holds |.((( lim_in_cod2 Rseq) . n) - z).| < (e / 2) by a5, a7;

 set N = ( max (N1,N2));



 a0: N is Nat by TARSKI: 1;

 for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( cod2_major_iterated_lim Rseq)).| < e

 proof

 let n, m;

 assume

 a10: n >= N & m >= N;

 N >= N1 & N >= N2 by XXREAL_0: 25;

 then n >= N1 & m >= N2 by a10, XXREAL_0: 2;

 then |.((Rseq . (n,m)) - (( lim_in_cod2 Rseq) . m)).| < (e / 2) & |.((( lim_in_cod2 Rseq) . m) - z).| < (e / 2) by a6, a9;

 then

 a12: ( |.((Rseq . (n,m)) - (( lim_in_cod2 Rseq) . m)).| + |.((( lim_in_cod2 Rseq) . m) - z).|) < ((e / 2) + (e / 2)) by XREAL_1: 8;

 |.((Rseq . (n,m)) - ( cod2_major_iterated_lim Rseq)).| <= ( |.((Rseq . (n,m)) - (( lim_in_cod2 Rseq) . m)).| + |.((( lim_in_cod2 Rseq) . m) - ( cod2_major_iterated_lim Rseq)).|) by COMPLEX1: 63;

 hence |.((Rseq . (n,m)) - ( cod2_major_iterated_lim Rseq)).| < e by a8, a12, XXREAL_0: 2;

 end;

 hence ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( cod2_major_iterated_lim Rseq)).| < e by a0;

 end;

 hence Rseq is P-convergent;

 hence thesis by a4, def6;

 end;

 definition

 let Rseq;

 :: DBLSEQ_1:def13

 attr Rseq is Cauchy means for e be Real st e > 0 holds ex N be Nat st for n1,n2,m1,m2 be Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds |.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e;

 end

 theorem :: DBLSEQ_1:7

 Rseq is P-convergent iff Rseq is Cauchy

 proof

 hereby

 assume

 a1: Rseq is P-convergent;

 now

 let e;

 assume

 a2: e > 0 ;

 consider z be Real such that

 a3: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - z).| < e by a1;

 consider N such that

 a4: for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - z).| < (e / 2) by a2, a3;

 now

 let n1,n2,m1,m2 be Nat;

 assume

 b1: N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2;

 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;

 end;

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

 end;

 hence Rseq is Cauchy;

 end;

 assume

 a6: Rseq is Cauchy;

 deffunc F( Element of NAT ) = (Rseq . ($1,$1));

 consider seq be Function of NAT , REAL such that

 a7: for n be Element of NAT holds (seq . n) = F(n) from FUNCT_2:sch 4;

 reconsider seq as Real_Sequence;

 now

 let e;

 assume e > 0 ;

 then

 consider N such that

 a8: for n1,n2,m1,m2 be Nat st N <= n1 & n1 <= n2 & N <= m1 & m1 <= m2 holds |.((Rseq . (n2,m2)) - (Rseq . (n1,m1))).| < e by a6;

 take N;

 hereby

 let n;



 c1: n is Element of NAT & N is Element of NAT by ORDINAL1:def 12;

 assume n >= N;

 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;

 end;

 end;

 then

 a11: seq is convergent by SEQ_4: 41;

 reconsider z = ( lim seq) as Complex;

 for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - z).| < e

 proof

 let e;

 assume

 a12: 0 < e;

 then

 consider N1 be Nat such that

 a13: for n st n >= N1 holds |.((seq . n) - ( lim seq)).| < (e / 2) by a11, SEQ_2:def 7;

 consider N2 be Nat such that

 a14: for n1,n2,m1,m2 be 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;

 hereby

 let n, m;



 c2: N is Element of NAT by ORDINAL1:def 12;

 assume

 a15: n >= N & m >= N;



 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;

 end;

 end;

 hence Rseq is P-convergent;

 end;

 theorem :: DBLSEQ_1:8

 for Rseq be Function of [: NAT , NAT :], REAL st Rseq is non-decreasing or Rseq is non-increasing holds Rseq is P-convergent iff Rseq is bounded_below bounded_above;

 definition

 let X,Y be non empty set;

 let H be BinOp of Y;

 let f,g be Function of X, Y;

 :: original: *

 redefine

 func H * (f,g) -> Function of [:X, X:], Y ;

 coherence

 proof



 a1: ( dom H) = [:Y, Y:] & ( dom f) = X & ( dom g) = X by FUNCT_2:def 1;



 a2: ( rng [:f, g:]) c= [:Y, Y:];

 ( dom (H * (f,g))) = ( dom (H * [:f, g:])) by FINSEQOP:def 4;

 then ( dom (H * (f,g))) = ( dom [:f, g:]) by a1, a2, RELAT_1: 27;

 then

 a3: ( dom (H * (f,g))) = [:X, X:] by FUNCT_2:def 1;

 ( rng (H * (f,g))) = ( rng (H * [:f, g:])) by FINSEQOP:def 4;

 then ( rng (H * (f,g))) c= ( rng H) & ( rng H) c= Y by RELAT_1: 26, RELAT_1:def 19;

 hence (H * (f,g)) is Function of [:X, X:], Y by a3, FUNCT_2: 2, XBOOLE_1: 1;

 end;

 end

 theorem :: DBLSEQ_1:9

 ( multreal * (rseq1,rseq2)) is convergent_in_cod1 convergent_in_cod2 & ( lim_in_cod1 ( multreal * (rseq1,rseq2))) is convergent & ( cod1_major_iterated_lim ( multreal * (rseq1,rseq2))) = (( lim rseq1) * ( lim rseq2)) & ( lim_in_cod2 ( multreal * (rseq1,rseq2))) is convergent & ( cod2_major_iterated_lim ( multreal * (rseq1,rseq2))) = (( lim rseq1) * ( lim rseq2)) & ( multreal * (rseq1,rseq2)) is P-convergent & ( P-lim ( multreal * (rseq1,rseq2))) = (( lim rseq1) * ( lim rseq2))

 proof

 set Rseq = ( multreal * (rseq1,rseq2));



 a2: for n, m holds (Rseq . (n,m)) = ((rseq1 . n) * (rseq2 . m))

 proof

 let n, m;



 a1: n in NAT & m in NAT by ORDINAL1:def 12;

 ( dom Rseq) = [: NAT , NAT :] by FUNCT_2:def 1;

 then [n, m] in ( dom Rseq) by a1, ZFMISC_1:def 2;

 then (Rseq . (n,m)) = ( multreal . ((rseq1 . n),(rseq2 . m))) by FINSEQOP: 77;

 hence (Rseq . (n,m)) = ((rseq1 . n) * (rseq2 . m)) by BINOP_2:def 11;

 end;



 x1: for m be Element of NAT , e be Real st 0 < e holds ex N st for n st n >= N holds |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) * (rseq2 . m))).| < e

 proof

 let m be Element of NAT , e be Real;

 assume

 a3: 0 < e;

 per cases ;

 suppose (rseq2 . m) <> 0 ;

 then

 a4: |.(rseq2 . m).| > 0 by COMPLEX1: 47;

 then

 consider N such that

 a5: for n st n >= N holds |.((rseq1 . n) - ( lim rseq1)).| < (e / |.(rseq2 . m).|) by a3, SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume n >= N;

 then

 a6: |.((rseq1 . n) - ( lim rseq1)).| < (e / |.(rseq2 . m).|) by a5;

 n is Element of NAT by ORDINAL1:def 12;



 then |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) * (rseq2 . m))).| = |.((Rseq . (n,m)) - (( lim rseq1) * (rseq2 . m))).| by MESFUNC9:def 7

 .= |.(((rseq1 . n) * (rseq2 . m)) - (( lim rseq1) * (rseq2 . m))).| by a2

 .= |.(((rseq1 . n) - ( lim rseq1)) * (rseq2 . m)).|

 .= ( |.((rseq1 . n) - ( lim rseq1)).| * |.(rseq2 . m).|) by COMPLEX1: 65;

 then |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) * (rseq2 . m))).| < ((e / |.(rseq2 . m).|) * |.(rseq2 . m).|) by a4, a6, XREAL_1: 68;

 hence |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) * (rseq2 . m))).| < e by a4, XCMPLX_1: 87;

 end;

 end;

 suppose

 a7: (rseq2 . m) = 0 ;

 take 0 ;

 hereby

 let n;

 assume n >= 0 ;

 n is Element of NAT by ORDINAL1:def 12;



 then |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) * (rseq2 . m))).| = |.((Rseq . (n,m)) - (( lim rseq1) * (rseq2 . m))).| by MESFUNC9:def 7

 .= |.(((rseq1 . n) * (rseq2 . m)) - (( lim rseq1) * (rseq2 . m))).| by a2

 .= 0 by a7, COMPLEX1: 44;

 hence |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) * (rseq2 . m))).| < e by a3;

 end;

 end;

 end;



 p1: for m be Element of NAT holds ( ProjMap2 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) * (rseq2 . m))).| < e by x1;

 hence ( ProjMap2 (Rseq,m)) is convergent by SEQ_2:def 6;

 end;

 hence Rseq is convergent_in_cod1;



 x2: for m be Element of NAT , e be Real st 0 < e holds ex N st for n st n >= N holds |.((( ProjMap1 (Rseq,m)) . n) - ((rseq1 . m) * ( lim rseq2))).| < e

 proof

 let m be Element of NAT , e be Real;

 assume

 a3: 0 < e;

 per cases ;

 suppose (rseq1 . m) <> 0 ;

 then

 a4: |.(rseq1 . m).| > 0 by COMPLEX1: 47;

 then

 consider N be Nat such that

 a5: for n be Nat st n >= N holds |.((rseq2 . n) - ( lim rseq2)).| < (e / |.(rseq1 . m).|) by a3, SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume n >= N;

 then

 a6: |.((rseq2 . n) - ( lim rseq2)).| < (e / |.(rseq1 . m).|) by a5;

 n is Element of NAT by ORDINAL1:def 12;



 then |.((( ProjMap1 (Rseq,m)) . n) - (( lim rseq2) * (rseq1 . m))).| = |.((Rseq . (m,n)) - (( lim rseq2) * (rseq1 . m))).| by MESFUNC9:def 6

 .= |.(((rseq2 . n) * (rseq1 . m)) - (( lim rseq2) * (rseq1 . m))).| by a2

 .= |.(((rseq2 . n) - ( lim rseq2)) * (rseq1 . m)).|

 .= ( |.((rseq2 . n) - ( lim rseq2)).| * |.(rseq1 . m).|) by COMPLEX1: 65;

 then |.((( ProjMap1 (Rseq,m)) . n) - (( lim rseq2) * (rseq1 . m))).| < ((e / |.(rseq1 . m).|) * |.(rseq1 . m).|) by a4, a6, XREAL_1: 68;

 hence |.((( ProjMap1 (Rseq,m)) . n) - ((rseq1 . m) * ( lim rseq2))).| < e by a4, XCMPLX_1: 87;

 end;

 end;

 suppose

 a7: (rseq1 . m) = 0 ;

 take 0 ;

 hereby

 let n;

 assume n >= 0 ;

 n is Element of NAT by ORDINAL1:def 12;



 then |.((( ProjMap1 (Rseq,m)) . n) - (( lim rseq2) * (rseq1 . m))).| = |.((Rseq . (m,n)) - (( lim rseq2) * (rseq1 . m))).| by MESFUNC9:def 6

 .= |.(((rseq2 . n) * (rseq1 . m)) - (( lim rseq2) * (rseq1 . m))).| by a2

 .= 0 by a7, COMPLEX1: 44;

 hence |.((( ProjMap1 (Rseq,m)) . n) - ((rseq1 . m) * ( lim rseq2))).| < e by a3;

 end;

 end;

 end;



 p2: for m be Element of NAT holds ( ProjMap1 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( ProjMap1 (Rseq,m)) . n) - ((rseq1 . m) * ( lim rseq2))).| < e by x2;

 hence ( ProjMap1 (Rseq,m)) is convergent by SEQ_2:def 6;

 end;

 hence Rseq is convergent_in_cod2;



 x3: for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| < e

 proof

 let e;

 assume

 a3: 0 < e;



 a6: for n holds (( lim_in_cod1 Rseq) . n) = (( lim rseq1) * (rseq2 . n))

 proof

 let n;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;



 a4: ( ProjMap2 (Rseq,n1)) is convergent by p1;



 a5: (( lim_in_cod1 Rseq) . n) = ( lim ( ProjMap2 (Rseq,n1))) by def32;

 for e st 0 < e holds ex N st for m st m >= N holds |.((( ProjMap2 (Rseq,n1)) . m) - (( lim rseq1) * (rseq2 . n))).| < e by x1;

 hence (( lim_in_cod1 Rseq) . n) = (( lim rseq1) * (rseq2 . n)) by a5, a4, SEQ_2:def 7;

 end;

 per cases by COMPLEX1: 46;

 suppose

 b1: |.( lim rseq1).| > 0 ;

 then

 consider N such that

 a7: for n st n >= N holds |.((rseq2 . n) - ( lim rseq2)).| < (e / |.( lim rseq1).|) by a3, SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume n >= N;

 then

 a8: |.((rseq2 . n) - ( lim rseq2)).| < (e / |.( lim rseq1).|) by a7;

 |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| = |.((( lim rseq1) * (rseq2 . n)) - (( lim rseq1) * ( lim rseq2))).| by a6

 .= |.(( lim rseq1) * ((rseq2 . n) - ( lim rseq2))).|

 .= ( |.( lim rseq1).| * |.((rseq2 . n) - ( lim rseq2)).|) by COMPLEX1: 65;

 hence |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| < e by a8, b1, XREAL_1: 79;

 end;

 end;

 suppose

 a9: |.( lim rseq1).| = 0 ;

 take 0 ;

 hereby

 let n;

 assume n >= 0 ;

 |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| = |.((( lim rseq1) * (rseq2 . n)) - (( lim rseq1) * ( lim rseq2))).| by a6

 .= |.(( lim rseq1) * ((rseq2 . n) - ( lim rseq2))).|

 .= ( |.( lim rseq1).| * |.((rseq2 . n) - ( lim rseq2)).|) by COMPLEX1: 65

 .= 0 by a9;

 hence |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| < e by a3;

 end;

 end;

 end;

 hence ( lim_in_cod1 Rseq) is convergent by SEQ_2:def 6;

 hence ( cod1_major_iterated_lim Rseq) = (( lim rseq1) * ( lim rseq2)) by x3, def34;



 x4: for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| < e

 proof

 let e;

 assume

 a3: 0 < e;



 a6: for n holds (( lim_in_cod2 Rseq) . n) = ((rseq1 . n) * ( lim rseq2))

 proof

 let n;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;



 a4: ( ProjMap1 (Rseq,n1)) is convergent by p2;



 a5: (( lim_in_cod2 Rseq) . n) = ( lim ( ProjMap1 (Rseq,n1))) by def33;

 for e st 0 < e holds ex N st for m st m >= N holds |.((( ProjMap1 (Rseq,n1)) . m) - ((rseq1 . n) * ( lim rseq2))).| < e by x2;

 hence (( lim_in_cod2 Rseq) . n) = ((rseq1 . n) * ( lim rseq2)) by a5, a4, SEQ_2:def 7;

 end;

 per cases by COMPLEX1: 46;

 suppose

 b1: |.( lim rseq2).| > 0 ;

 then

 consider N such that

 a7: for n st n >= N holds |.((rseq1 . n) - ( lim rseq1)).| < (e / |.( lim rseq2).|) by a3, SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume n >= N;

 then

 a8: |.((rseq1 . n) - ( lim rseq1)).| < (e / |.( lim rseq2).|) by a7;

 |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| = |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).| by a6

 .= |.(((rseq1 . n) - ( lim rseq1)) * ( lim rseq2)).|

 .= ( |.( lim rseq2).| * |.((rseq1 . n) - ( lim rseq1)).|) by COMPLEX1: 65;

 hence |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| < e by a8, b1, XREAL_1: 79;

 end;

 end;

 suppose

 a9: |.( lim rseq2).| = 0 ;

 take 0 ;

 hereby

 let n;

 assume n >= 0 ;

 |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| = |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).| by a6

 .= |.(( lim rseq2) * ((rseq1 . n) - ( lim rseq1))).|

 .= ( |.( lim rseq2).| * |.((rseq1 . n) - ( lim rseq1)).|) by COMPLEX1: 65

 .= 0 by a9;

 hence |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) * ( lim rseq2))).| < e by a3;

 end;

 end;

 end;

 hence ( lim_in_cod2 Rseq) is convergent by SEQ_2:def 6;

 hence ( cod2_major_iterated_lim Rseq) = (( lim rseq1) * ( lim rseq2)) by x4, def35;



 x5: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - (( lim rseq1) * ( lim rseq2))).| < e

 proof

 let e;

 assume

 c1: 0 < e;

 consider K be Real such that

 c2: 0 < K & for n holds |.(rseq1 . n).| < K by SEQ_2: 3;

 set b = ( max (K, |.( lim rseq2).|));



 c10: b >= K & b >= |.( lim rseq2).| by XXREAL_0: 25;

 then

 consider N1 be Nat such that

 c4: for n st n >= N1 holds |.((rseq1 . n) - ( lim rseq1)).| < (e / (2 * b)) by c1, c2, SEQ_2:def 7;

 consider N2 be Nat such that

 c5: for n st n >= N2 holds |.((rseq2 . n) - ( lim rseq2)).| < (e / (2 * b)) by c1, c2, c10, SEQ_2:def 7;

 reconsider N = ( max (N1,N2)) as Nat by TARSKI: 1;

 take N;

 thus for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - (( lim rseq1) * ( lim rseq2))).| < e

 proof

 let n, m;

 assume

 c13: n >= N & m >= N;

 ( max (N1,N2)) >= N1 & ( max (N1,N2)) >= N2 by XXREAL_0: 25;

 then

 c6: n >= N1 & m >= N2 by c13, XXREAL_0: 2;



 c7: |.((Rseq . (n,m)) - (( lim rseq1) * ( lim rseq2))).| <= ( |.((Rseq . (n,m)) - ((rseq1 . n) * ( lim rseq2))).| + |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).|) by COMPLEX1: 63;



 c11: |.((rseq1 . n) - ( lim rseq1)).| >= 0 & |.((rseq2 . m) - ( lim rseq2)).| >= 0 by COMPLEX1: 46;



 c12: |.(rseq1 . n).| < b & |.( lim rseq2).| <= b by c2, c10, XXREAL_0: 2;

 |.((Rseq . (n,m)) - ((rseq1 . n) * ( lim rseq2))).| = |.(((rseq1 . n) * (rseq2 . m)) - ((rseq1 . n) * ( lim rseq2))).| by a2

 .= |.((rseq1 . n) * ((rseq2 . m) - ( lim rseq2))).|

 .= ( |.(rseq1 . n).| * |.((rseq2 . m) - ( lim rseq2)).|) by COMPLEX1: 65;

 then

 c8: |.((Rseq . (n,m)) - ((rseq1 . n) * ( lim rseq2))).| <= (b * |.((rseq2 . m) - ( lim rseq2)).|) by c11, c12, XREAL_1: 64;

 |.((rseq2 . m) - ( lim rseq2)).| < (e / (2 * b)) by c5, c6;

 then (b * |.((rseq2 . m) - ( lim rseq2)).|) < (b * (e / (2 * b))) by c2, c10, XREAL_1: 68;

 then |.((Rseq . (n,m)) - ((rseq1 . n) * ( lim rseq2))).| < (b * (e / (2 * b))) by c8, XXREAL_0: 2;

 then |.((Rseq . (n,m)) - ((rseq1 . n) * ( lim rseq2))).| < (e / ((2 * b) / b)) by XCMPLX_1: 81;

 then

 c15: |.((Rseq . (n,m)) - ((rseq1 . n) * ( lim rseq2))).| < (e / 2) by c2, c10, XCMPLX_1: 89;

 |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).| = |.(( lim rseq2) * ((rseq1 . n) - ( lim rseq1))).|

 .= ( |.( lim rseq2).| * |.((rseq1 . n) - ( lim rseq1)).|) by COMPLEX1: 65;

 then

 c9: |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).| <= (b * |.((rseq1 . n) - ( lim rseq1)).|) by c11, XXREAL_0: 25, XREAL_1: 64;

 |.((rseq1 . n) - ( lim rseq1)).| < (e / (2 * b)) by c4, c6;

 then (b * |.((rseq1 . n) - ( lim rseq1)).|) < (b * (e / (2 * b))) by c2, c10, XREAL_1: 68;

 then |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).| < (b * (e / (2 * b))) by c9, XXREAL_0: 2;

 then |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).| < (e / ((2 * b) / b)) by XCMPLX_1: 81;

 then |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).| < (e / 2) by c2, c10, XCMPLX_1: 89;

 then ( |.((Rseq . (n,m)) - ((rseq1 . n) * ( lim rseq2))).| + |.(((rseq1 . n) * ( lim rseq2)) - (( lim rseq1) * ( lim rseq2))).|) < ((e / 2) + (e / 2)) by c15, XREAL_1: 8;

 hence |.((Rseq . (n,m)) - (( lim rseq1) * ( lim rseq2))).| < e by c7, XXREAL_0: 2;

 end;

 end;

 hence Rseq is P-convergent;

 hence ( P-lim Rseq) = (( lim rseq1) * ( lim rseq2)) by x5, def6;

 end;

 theorem :: DBLSEQ_1:10

 ( addreal * (rseq1,rseq2)) is convergent_in_cod1 convergent_in_cod2 & ( lim_in_cod1 ( addreal * (rseq1,rseq2))) is convergent & ( cod1_major_iterated_lim ( addreal * (rseq1,rseq2))) = (( lim rseq1) + ( lim rseq2)) & ( lim_in_cod2 ( addreal * (rseq1,rseq2))) is convergent & ( cod2_major_iterated_lim ( addreal * (rseq1,rseq2))) = (( lim rseq1) + ( lim rseq2)) & ( addreal * (rseq1,rseq2)) is P-convergent & ( P-lim ( addreal * (rseq1,rseq2))) = (( lim rseq1) + ( lim rseq2))

 proof

 set Rseq = ( addreal * (rseq1,rseq2));



 a2: for n, m holds (Rseq . (n,m)) = ((rseq1 . n) + (rseq2 . m))

 proof

 let n, m;



 a1: n in NAT & m in NAT by ORDINAL1:def 12;

 ( dom Rseq) = [: NAT , NAT :] by FUNCT_2:def 1;

 then [n, m] in ( dom Rseq) by a1, ZFMISC_1:def 2;

 then (Rseq . (n,m)) = ( addreal . ((rseq1 . n),(rseq2 . m))) by FINSEQOP: 77;

 hence (Rseq . (n,m)) = ((rseq1 . n) + (rseq2 . m)) by BINOP_2:def 9;

 end;



 x1: for m be Element of NAT , e be Real st 0 < e holds ex N be Nat st for n be Nat st n >= N holds |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) + (rseq2 . m))).| < e

 proof

 let m be Element of NAT , e be Real;

 assume 0 < e;

 then

 consider N be Nat such that

 a3: for n be Nat st n >= N holds |.((rseq1 . n) - ( lim rseq1)).| < e by SEQ_2:def 7;

 take N;

 hereby

 let n be Nat;

 assume

 a4: n >= N;

 n is Element of NAT by ORDINAL1:def 12;



 then |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) + (rseq2 . m))).| = |.((Rseq . (n,m)) - (( lim rseq1) + (rseq2 . m))).| by MESFUNC9:def 7

 .= |.(((rseq1 . n) + (rseq2 . m)) - (( lim rseq1) + (rseq2 . m))).| by a2

 .= |.((rseq1 . n) - ( lim rseq1)).|;

 hence |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) + (rseq2 . m))).| < e by a3, a4;

 end;

 end;



 p1: for m be Element of NAT holds ( ProjMap2 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( ProjMap2 (Rseq,m)) . n) - (( lim rseq1) + (rseq2 . m))).| < e by x1;

 hence ( ProjMap2 (Rseq,m)) is convergent by SEQ_2:def 6;

 end;

 hence Rseq is convergent_in_cod1;



 x2: for m be Element of NAT , e be Real st 0 < e holds ex N st for n st n >= N holds |.((( ProjMap1 (Rseq,m)) . n) - ((rseq1 . m) + ( lim rseq2))).| < e

 proof

 let m be Element of NAT , e be Real;

 assume 0 < e;

 then

 consider N such that

 a3: for n st n >= N holds |.((rseq2 . n) - ( lim rseq2)).| < e by SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume

 a4: n >= N;

 n is Element of NAT by ORDINAL1:def 12;



 then |.((( ProjMap1 (Rseq,m)) . n) - (( lim rseq2) + (rseq1 . m))).| = |.((Rseq . (m,n)) - (( lim rseq2) + (rseq1 . m))).| by MESFUNC9:def 6

 .= |.(((rseq2 . n) + (rseq1 . m)) - (( lim rseq2) + (rseq1 . m))).| by a2

 .= |.((rseq2 . n) - ( lim rseq2)).|;

 hence |.((( ProjMap1 (Rseq,m)) . n) - ((rseq1 . m) + ( lim rseq2))).| < e by a3, a4;

 end;

 end;



 p2: for m be Element of NAT holds ( ProjMap1 (Rseq,m)) is convergent

 proof

 let m be Element of NAT ;

 for e st 0 < e holds ex N st for n st n >= N holds |.((( ProjMap1 (Rseq,m)) . n) - ((rseq1 . m) + ( lim rseq2))).| < e by x2;

 hence ( ProjMap1 (Rseq,m)) is convergent by SEQ_2:def 6;

 end;

 hence Rseq is convergent_in_cod2;



 x3: for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) + ( lim rseq2))).| < e

 proof

 let e;

 assume 0 < e;

 then

 consider N such that

 a3: for n st n >= N holds |.((rseq2 . n) - ( lim rseq2)).| < e by SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume n >= N;

 then

 a4: |.((rseq2 . n) - ( lim rseq2)).| < e by a3;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;



 a5: ( ProjMap2 (Rseq,n1)) is convergent by p1;



 a6: (( lim_in_cod1 Rseq) . n) = ( lim ( ProjMap2 (Rseq,n1))) by def32;

 for e st 0 < e holds ex N st for m st m >= N holds |.((( ProjMap2 (Rseq,n1)) . m) - (( lim rseq1) + (rseq2 . n))).| < e by x1;

 then |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) + ( lim rseq2))).| = |.((( lim rseq1) + (rseq2 . n)) - (( lim rseq1) + ( lim rseq2))).| by a5, a6, SEQ_2:def 7;

 hence |.((( lim_in_cod1 Rseq) . n) - (( lim rseq1) + ( lim rseq2))).| < e by a4;

 end;

 end;

 hence ( lim_in_cod1 Rseq) is convergent by SEQ_2:def 6;

 hence ( cod1_major_iterated_lim Rseq) = (( lim rseq1) + ( lim rseq2)) by x3, def34;



 x4: for e st 0 < e holds ex N st for n st n >= N holds |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) + ( lim rseq2))).| < e

 proof

 let e;

 assume 0 < e;

 then

 consider N such that

 a3: for n st n >= N holds |.((rseq1 . n) - ( lim rseq1)).| < e by SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume n >= N;

 then

 a4: |.((rseq1 . n) - ( lim rseq1)).| < e by a3;

 reconsider n1 = n as Element of NAT by ORDINAL1:def 12;



 a5: ( ProjMap1 (Rseq,n1)) is convergent by p2;



 a6: (( lim_in_cod2 Rseq) . n) = ( lim ( ProjMap1 (Rseq,n1))) by def33;

 for e st 0 < e holds ex N st for m st m >= N holds |.((( ProjMap1 (Rseq,n1)) . m) - ((rseq1 . n) + ( lim rseq2))).| < e by x2;

 then |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) + ( lim rseq2))).| = |.(((rseq1 . n) + ( lim rseq2)) - (( lim rseq1) + ( lim rseq2))).| by a5, a6, SEQ_2:def 7;

 hence |.((( lim_in_cod2 Rseq) . n) - (( lim rseq1) + ( lim rseq2))).| < e by a4;

 end;

 end;

 hence ( lim_in_cod2 Rseq) is convergent by SEQ_2:def 6;

 hence ( cod2_major_iterated_lim Rseq) = (( lim rseq1) + ( lim rseq2)) by x4, def35;



 x5: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - (( lim rseq1) + ( lim rseq2))).| < e

 proof

 let e;

 assume

 c1: 0 < e;

 then

 consider N1 be Nat such that

 c4: for n st n >= N1 holds |.((rseq1 . n) - ( lim rseq1)).| < (e / 2) by SEQ_2:def 7;

 consider N2 be Nat such that

 c5: for n st n >= N2 holds |.((rseq2 . n) - ( lim rseq2)).| < (e / 2) by c1, SEQ_2:def 7;

 reconsider N = ( max (N1,N2)) as Nat by TARSKI: 1;

 take N;

 thus for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - (( lim rseq1) + ( lim rseq2))).| < e

 proof

 let n, m;

 assume

 c13: n >= N & m >= N;

 ( max (N1,N2)) >= N1 & ( max (N1,N2)) >= N2 by XXREAL_0: 25;

 then

 c6: n >= N1 & m >= N2 by c13, XXREAL_0: 2;

 |.((Rseq . (n,m)) - (( lim rseq1) + ( lim rseq2))).| = |.(((rseq1 . n) + (rseq2 . m)) - (( lim rseq1) + ( lim rseq2))).| by a2

 .= |.(((rseq1 . n) - ( lim rseq1)) + ((rseq2 . m) - ( lim rseq2))).|;

 then

 a8: |.((Rseq . (n,m)) - (( lim rseq1) + ( lim rseq2))).| <= ( |.((rseq1 . n) - ( lim rseq1)).| + |.((rseq2 . m) - ( lim rseq2)).|) by COMPLEX1: 56;

 |.((rseq1 . n) - ( lim rseq1)).| < (e / 2) & |.((rseq2 . m) - ( lim rseq2)).| < (e / 2) by c4, c5, c6;

 then ( |.((rseq1 . n) - ( lim rseq1)).| + |.((rseq2 . m) - ( lim rseq2)).|) < ((e / 2) + (e / 2)) by XREAL_1: 8;

 hence |.((Rseq . (n,m)) - (( lim rseq1) + ( lim rseq2))).| < e by a8, XXREAL_0: 2;

 end;

 end;

 hence Rseq is P-convergent;

 hence ( P-lim Rseq) = (( lim rseq1) + ( lim rseq2)) by x5, def6;

 end;



 lmADD: for Rseq1,Rseq2 be Function of [: NAT , NAT :], REAL holds ( dom (Rseq1 + Rseq2)) = [: NAT , NAT :] & ( dom (Rseq1 - Rseq2)) = [: NAT , NAT :] & (for n,m be Nat holds ((Rseq1 + Rseq2) . (n,m)) = ((Rseq1 . (n,m)) + (Rseq2 . (n,m)))) & (for n,m be Nat holds ((Rseq1 - Rseq2) . (n,m)) = ((Rseq1 . (n,m)) - (Rseq2 . (n,m))))

 proof

 let Rseq1,Rseq2 be Function of [: NAT , NAT :], REAL ;

 thus

 a1: ( dom (Rseq1 + Rseq2)) = [: NAT , NAT :] & ( dom (Rseq1 - Rseq2)) = [: NAT , NAT :] by FUNCT_2:def 1;

 hereby

 let n, m;

 n in NAT & m in NAT by ORDINAL1:def 12;

 hence ((Rseq1 + Rseq2) . (n,m)) = ((Rseq1 . (n,m)) + (Rseq2 . (n,m))) by VALUED_1:def 1, a1, ZFMISC_1: 87;

 end;

 hereby

 let n, m;

 n in NAT & m in NAT by ORDINAL1:def 12;

 hence ((Rseq1 - Rseq2) . (n,m)) = ((Rseq1 . (n,m)) - (Rseq2 . (n,m))) by VALUED_1: 13, a1, ZFMISC_1: 87;

 end;

 end;

 theorem :: DBLSEQ_1:11

 Rseq1 is P-convergent & Rseq2 is P-convergent implies (Rseq1 + Rseq2) is P-convergent & ( P-lim (Rseq1 + Rseq2)) = (( P-lim Rseq1) + ( P-lim Rseq2))

 proof

 assume

 a1: Rseq1 is P-convergent & Rseq2 is P-convergent;

 a2:

 now

 let e;

 assume

 a4: 0 < e;

 then

 consider N1 be Nat such that

 a5: for n, m st n >= N1 & m >= N1 holds |.((Rseq1 . (n,m)) - ( P-lim Rseq1)).| < (e / 2) by a1, def6;

 consider N2 be Nat such that

 a6: for n, m 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;

 now

 let n, m;

 assume

 a8: n >= N & m >= N;

 N >= N1 & N >= N2 by XXREAL_0: 25;

 then n >= N1 & n >= N2 & m >= N1 & m >= N2 by a8, XXREAL_0: 2;

 then |.((Rseq1 . (n,m)) - ( P-lim Rseq1)).| < (e / 2) & |.((Rseq2 . (n,m)) - ( P-lim Rseq2)).| < (e / 2) by a5, a6;

 then

 a9: ( |.((Rseq1 . (n,m)) - ( P-lim Rseq1)).| + |.((Rseq2 . (n,m)) - ( P-lim Rseq2)).|) < ((e / 2) + (e / 2)) by 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)) + ((Rseq2 . (n,m)) - ( P-lim Rseq2)));

 then |.(((Rseq1 + Rseq2) . (n,m)) - (( P-lim Rseq1) + ( P-lim Rseq2))).| <= ( |.((Rseq1 . (n,m)) - ( P-lim Rseq1)).| + |.((Rseq2 . (n,m)) - ( P-lim Rseq2)).|) by COMPLEX1: 56;

 hence |.(((Rseq1 + Rseq2) . (n,m)) - (( P-lim Rseq1) + ( P-lim Rseq2))).| < e by a9, XXREAL_0: 2;

 end;

 hence for n,m be Nat st n >= N & m >= N holds |.(((Rseq1 + Rseq2) . (n,m)) - (( P-lim Rseq1) + ( P-lim Rseq2))).| < e;

 end;

 hence (Rseq1 + Rseq2) is P-convergent;

 hence thesis by a2, def6;

 end;

 theorem :: DBLSEQ_1:12



 th54b: Rseq1 is P-convergent & Rseq2 is P-convergent implies (Rseq1 - Rseq2) is P-convergent & ( P-lim (Rseq1 - Rseq2)) = (( P-lim Rseq1) - ( P-lim Rseq2))

 proof

 assume

 a1: Rseq1 is P-convergent & Rseq2 is P-convergent;

 a2:

 now

 let e;

 assume

 a4: 0 < e;

 then

 consider N1 be Nat such that

 a5: for n, m st n >= N1 & m >= N1 holds |.((Rseq1 . (n,m)) - ( P-lim Rseq1)).| < (e / 2) by a1, def6;

 consider N2 be Nat such that

 a6: for n, m 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;

 now

 let n, m;

 assume

 a8: n >= N & m >= N;

 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;

 end;

 hence for n,m be Nat st n >= N & m >= N holds |.(((Rseq1 - Rseq2) . (n,m)) - (( P-lim Rseq1) - ( P-lim Rseq2))).| < e;

 end;

 hence (Rseq1 - Rseq2) is P-convergent;

 hence thesis by a2, def6;

 end;



 lm55a: for a be Real st (for n,m be Nat holds (Rseq . (n,m)) = a) holds Rseq is P-convergent & ( P-lim Rseq) = a

 proof

 let a be Real;

 assume

 a1: for n,m be Nat holds (Rseq . (n,m)) = a;

 a3:

 now

 let e be Real;

 assume

 a2: 0 < e;

 a4:

 now

 let n, m such that n >= 0 & m >= 0 ;

 (Rseq . (n,m)) = a by a1;

 hence |.((Rseq . (n,m)) - a).| < e by a2, COMPLEX1: 44;

 end;

 reconsider N = 0 as Nat;

 take N;

 thus for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - a).| < e by a4;

 end;

 hence Rseq is P-convergent;

 hence ( P-lim Rseq) = a by a3, def6;

 end;

 theorem :: DBLSEQ_1:13

 for Rseq be Function of [: NAT , NAT :], REAL , r be Real st Rseq is P-convergent holds (r (#) Rseq) is P-convergent & ( P-lim (r (#) Rseq)) = (r * ( P-lim Rseq))

 proof

 let Rseq be Function of [: NAT , NAT :], REAL ;

 let r be Real;

 assume

 a1: Rseq is P-convergent;

 a4:

 now

 assume

 a2: r = 0 ;

 a3:

 now

 let n, m;

 ((r (#) Rseq) . (n,m)) = (r * (Rseq . (n,m))) by VALUED_1: 6;

 hence ((r (#) Rseq) . (n,m)) = 0 by a2;

 end;

 hence (r (#) Rseq) is P-convergent by lm55a;

 thus ( P-lim (r (#) Rseq)) = 0 by a3, lm55a;

 end;

 now

 assume r <> 0 ;

 then

 a5: |.r.| > 0 by COMPLEX1: 47;

 a7:

 now

 let e be Real;

 assume 0 < e;

 then

 consider N such that

 a6: for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( P-lim Rseq)).| < (e / |.r.|) by a1, a5, def6;

 take N;

 hereby

 let n, m;

 assume n >= N & m >= N;

 then |.((Rseq . (n,m)) - ( P-lim Rseq)).| < (e / |.r.|) by a6;

 then ( |.r.| * |.((Rseq . (n,m)) - ( P-lim Rseq)).|) < ((e / |.r.|) * |.r.|) by a5, XREAL_1: 68;

 then ( |.r.| * |.((Rseq . (n,m)) - ( P-lim Rseq)).|) < ( |.r.| / ( |.r.| / e)) by XCMPLX_1: 79;

 then ( |.r.| * |.((Rseq . (n,m)) - ( P-lim Rseq)).|) < e by a5, XCMPLX_1: 52;

 then |.(r * ((Rseq . (n,m)) - ( P-lim Rseq))).| < e by COMPLEX1: 65;

 then |.((r * (Rseq . (n,m))) - (r * ( P-lim Rseq))).| < e;

 hence |.(((r (#) Rseq) . (n,m)) - (r * ( P-lim Rseq))).| < e by VALUED_1: 6;

 end;

 end;

 hence (r (#) Rseq) is P-convergent;

 hence ( P-lim (r (#) Rseq)) = (r * ( P-lim Rseq)) by a7, def6;

 end;

 hence thesis by a4;

 end;

 theorem :: DBLSEQ_1:14



 th55b: Rseq is P-convergent & (for n,m be Nat holds (Rseq . (n,m)) >= r) implies ( P-lim Rseq) >= r

 proof

 assume

 a1: Rseq is P-convergent;

 assume

 a2: for n,m be Nat holds (Rseq . (n,m)) >= r;

 assume not ( P-lim Rseq) >= r;

 then (r - ( P-lim Rseq)) > 0 by XREAL_1: 50;

 then

 consider N such that

 a3: for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( P-lim Rseq)).| < (r - ( P-lim Rseq)) by a1, def6;

 |.((Rseq . (N,N)) - ( P-lim Rseq)).| < (r - ( P-lim Rseq)) by a3;

 then (( P-lim Rseq) + (r - ( P-lim Rseq))) > (Rseq . (N,N)) by RINFSUP1: 1;

 hence contradiction by a2;

 end;

 theorem :: DBLSEQ_1:15

 Rseq1 is P-convergent & Rseq2 is P-convergent & (for n,m be Nat holds (Rseq1 . (n,m)) <= (Rseq2 . (n,m))) implies ( P-lim Rseq1) <= ( P-lim Rseq2)

 proof

 assume

 a1: Rseq1 is P-convergent & Rseq2 is P-convergent;

 assume

 a2: for n,m be Nat holds (Rseq1 . (n,m)) <= (Rseq2 . (n,m));



 a3: (Rseq2 - Rseq1) is P-convergent & ( P-lim (Rseq2 - Rseq1)) = (( P-lim Rseq2) - ( P-lim Rseq1)) by a1, th54b;

 now

 let n, m;

 ((Rseq2 - Rseq1) . (n,m)) = ((Rseq2 . (n,m)) - (Rseq1 . (n,m))) by lmADD;

 hence ((Rseq2 - Rseq1) . (n,m)) >= 0 by a2, XREAL_1: 48;

 end;

 hence ( P-lim Rseq1) <= ( P-lim Rseq2) by a3, th55b, XREAL_1: 49;

 end;

 theorem :: DBLSEQ_1:16

 Rseq1 is P-convergent & Rseq2 is P-convergent & ( P-lim Rseq1) = ( P-lim Rseq2) & (for n,m be 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)

 proof

 assume that

 a1: Rseq1 is P-convergent & Rseq2 is P-convergent and

 a2: ( P-lim Rseq1) = ( P-lim Rseq2) and

 a3: for n,m be Nat holds (Rseq1 . (n,m)) <= (Rseq . (n,m)) & (Rseq . (n,m)) <= (Rseq2 . (n,m));



 a4: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( P-lim Rseq1)).| < e

 proof

 let e;

 assume

 a5: 0 < e;

 then

 consider N1 be Nat such that

 a6: for n, m st n >= N1 & m >= N1 holds |.((Rseq1 . (n,m)) - ( P-lim Rseq1)).| < e by a1, def6;

 consider N2 be Nat such that

 a7: for n, m 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;



 a8: ( max (N1,N2)) >= N1 & ( max (N1,N2)) >= N2 by XXREAL_0: 25;

 hereby

 let n, m;

 assume n >= N & m >= N;

 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;

 end;

 end;

 hence Rseq is P-convergent;

 hence ( P-lim Rseq) = ( P-lim Rseq1) by a4, def6;

 end;

 definition

 let X be non empty set, seq be Function of [: NAT , NAT :], X;

 :: DBLSEQ_1:def14

 mode subsequence of seq -> Function of [: NAT , NAT :], X means

 : def9: ex N,M be increasing sequence of NAT st for n,m be Nat holds (it . (n,m)) = (seq . ((N . n),(M . m)));

 existence

 proof

 deffunc F( object, object) = (seq . ((( id NAT ) . $1),(( id NAT ) . $2)));

 consider s be Function such that

 a1: ( dom s) = [: NAT , NAT :] & for n,m be object st n in NAT & m in NAT holds (s . (n,m)) = F(n,m) from FUNCT_3:sch 2;

 for z be object st z in [: NAT , NAT :] holds (s . z) in X

 proof

 let z be object;

 assume z in [: NAT , NAT :];

 then

 consider n,m be object such that

 a2: n in NAT & m in NAT & z = [n, m] by ZFMISC_1:def 2;

 reconsider n, m as Nat by a2;

 (s . z) = (s . (n,m)) by a2;

 then (s . z) = (seq . ((( id NAT ) . n),(( id NAT ) . m))) by a1, a2;

 hence (s . z) in X;

 end;

 then

 reconsider s as Function of [: NAT , NAT :], X by a1, FUNCT_2: 3;

 take s, ( id NAT ), ( id NAT );

 hereby

 let n,m be Nat;

 n is Element of NAT & m is Element of NAT by ORDINAL1:def 12;

 hence (s . (n,m)) = (seq . ((( id NAT ) . n),(( id NAT ) . m))) by a1;

 end;

 end;

 end



 lem01: for seq be increasing sequence of NAT , n be Nat holds n <= (seq . n)

 proof

 let seq be increasing sequence of NAT ;

 let n be Nat;



 a1: seq is Real_Sequence by FUNCT_2: 7, NUMBERS: 19;

 ( rng seq) c= NAT by RELAT_1:def 19;

 hence n <= (seq . n) by a1, HEINE: 2;

 end;



 LM114: for Rseq1 be subsequence of Rseq st Rseq is P-convergent holds Rseq1 is P-convergent & ( P-lim Rseq1) = ( P-lim Rseq)

 proof

 let Rseq1 be subsequence of Rseq;

 assume

 a1: Rseq is P-convergent;



 a2: for e st 0 < e holds ex N st for n, m st n >= N & m >= N holds |.((Rseq1 . (n,m)) - ( P-lim Rseq)).| < e

 proof

 let e;

 assume 0 < e;

 then

 consider N such that

 a3: for n, m st n >= N & m >= N holds |.((Rseq . (n,m)) - ( P-lim Rseq)).| < e by a1, def6;

 take N;

 hereby

 let n, m;

 assume

 a4: n >= N & m >= N;

 consider I1,I2 be increasing sequence of NAT such that

 a5: for n, m holds (Rseq1 . (n,m)) = (Rseq . ((I1 . n),(I2 . m))) by def9;

 (I1 . n) >= n & (I2 . m) >= m by lem01;

 then (I1 . n) >= N & (I2 . m) >= N by a4, XXREAL_0: 2;

 then |.((Rseq . ((I1 . n),(I2 . m))) - ( P-lim Rseq)).| < e by a3;

 hence |.((Rseq1 . (n,m)) - ( P-lim Rseq)).| < e by a5;

 end;

 end;

 hence Rseq1 is P-convergent;

 hence ( P-lim Rseq1) = ( P-lim Rseq) by a2, def6;

 end;



 th63d: Rseq is convergent_in_cod1 implies for Rseq1 be subsequence of Rseq holds Rseq1 is convergent_in_cod1

 proof

 assume

 a1: Rseq is convergent_in_cod1;

 hereby

 let Rseq1 be subsequence of Rseq;

 consider I1,I2 be increasing sequence of NAT such that

 a7: for n, m holds (Rseq1 . (n,m)) = (Rseq . ((I1 . n),(I2 . m))) by def9;

 for m be Element of NAT holds ( ProjMap2 (Rseq1,m)) is convergent

 proof

 let m be Element of NAT ;

 reconsider m2 = (I2 . m) as Element of NAT ;



 a4: ( ProjMap2 (Rseq,m2)) is convergent by a1;

 now

 let e be Real;

 assume 0 < e;

 then

 consider N such that

 a5: for n st n >= N holds |.((( ProjMap2 (Rseq,m2)) . n) - ( lim ( ProjMap2 (Rseq,m2)))).| < e by a4, SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume

 a6: n >= N;



 x1: (I1 . n) is Element of NAT & n is Element of NAT by ORDINAL1:def 12;

 (I1 . n) >= n by lem01;

 then (I1 . n) >= N by a6, XXREAL_0: 2;

 then |.((( ProjMap2 (Rseq,m2)) . (I1 . n)) - ( lim ( ProjMap2 (Rseq,m2)))).| < e by a5;

 then |.((Rseq . ((I1 . n),(I2 . m))) - ( lim ( ProjMap2 (Rseq,m2)))).| < e by MESFUNC9:def 7;

 then |.((Rseq1 . (n,m)) - ( lim ( ProjMap2 (Rseq,m2)))).| < e by a7;

 hence |.((( ProjMap2 (Rseq1,m)) . n) - ( lim ( ProjMap2 (Rseq,m2)))).| < e by x1, MESFUNC9:def 7;

 end;

 end;

 hence ( ProjMap2 (Rseq1,m)) is convergent by SEQ_2:def 6;

 end;

 hence Rseq1 is convergent_in_cod1;

 end;

 end;

 registration

 let Pseq;

 cluster -> P-convergent for subsequence of Pseq;

 coherence by LM114;

 end

 theorem :: DBLSEQ_1:17

 for Psubseq be subsequence of Pseq holds ( P-lim Psubseq) = ( P-lim Pseq) by LM114;

 registration

 let Rseq be convergent_in_cod1 Function of [: NAT , NAT :], REAL ;

 cluster -> convergent_in_cod1 for subsequence of Rseq;

 coherence by th63d;

 end

 theorem :: DBLSEQ_1:18

 for Rseq1 be subsequence of Rseq st Rseq is convergent_in_cod1 & ( lim_in_cod1 Rseq) is convergent holds ( lim_in_cod1 Rseq1) is convergent & ( cod1_major_iterated_lim Rseq1) = ( cod1_major_iterated_lim Rseq)

 proof

 let Rseq1 be subsequence of Rseq;

 assume that

 a1: Rseq is convergent_in_cod1 & ( lim_in_cod1 Rseq) is convergent;

 consider I1,I2 be increasing sequence of NAT such that

 a7: for n,m be Nat holds (Rseq1 . (n,m)) = (Rseq . ((I1 . n),(I2 . m))) by def9;



 a8: Rseq1 is convergent_in_cod1 by a1;



 a10: for e st 0 < e holds ex N st for m st m >= N holds |.((( lim_in_cod1 Rseq1) . m) - ( cod1_major_iterated_lim Rseq)).| < e

 proof

 let e;

 assume 0 < e;

 then

 consider N such that

 a11: for m st m >= N holds |.((( lim_in_cod1 Rseq) . m) - ( cod1_major_iterated_lim Rseq)).| < e by a1, def34;

 take N;

 hereby

 let m;

 assume

 a12: m >= N;

 reconsider m2 = (I2 . m) as Element of NAT ;

 reconsider m1 = m as Element of NAT by ORDINAL1:def 12;



 x2: ( ProjMap2 (Rseq1,m1)) is convergent by a8;

 for p be Real st 0 = K holds |.((( ProjMap2 (Rseq1,m1)) . n) - ( lim ( ProjMap2 (Rseq,m2)))).| < p

 proof

 let p be Real;

 assume

 b1: 0 < p;

 ( ProjMap2 (Rseq,m2)) is convergent by a1;

 then

 consider K be Nat such that

 b2: for n st n >= K holds |.((( ProjMap2 (Rseq,m2)) . n) - ( lim ( ProjMap2 (Rseq,m2)))).| = K;



 x2: n is Element of NAT & (I1 . n) is Element of NAT & (I2 . m) is Element of NAT by ORDINAL1:def 12;

 (I1 . n) >= n by lem01;

 then (I1 . n) >= K by b3, XXREAL_0: 2;

 then |.((( ProjMap2 (Rseq,m2)) . (I1 . n)) - ( lim ( ProjMap2 (Rseq,m2)))).| < p by b2;

 then |.((Rseq . ((I1 . n),(I2 . m))) - ( lim ( ProjMap2 (Rseq,m2)))).| < p by MESFUNC9:def 7;

 then |.((Rseq1 . (n,m)) - ( lim ( ProjMap2 (Rseq,m2)))).| < p by a7;

 hence |.((( ProjMap2 (Rseq1,m1)) . n) - ( lim ( ProjMap2 (Rseq,m2)))).| = m by lem01;

 then (I2 . m) >= N by a12, XXREAL_0: 2;

 then

 a13: |.((( lim_in_cod1 Rseq) . (I2 . m)) - ( cod1_major_iterated_lim Rseq)).| < e by a11;

 (( lim_in_cod1 Rseq) . (I2 . m)) = ( lim ( ProjMap2 (Rseq,m2))) by def32;

 hence |.((( lim_in_cod1 Rseq1) . m) - ( cod1_major_iterated_lim Rseq)).| < e by def32, a13, c1;

 end;

 end;

 hence ( lim_in_cod1 Rseq1) is convergent by SEQ_2:def 6;

 hence thesis by a10, def34;

 end;



 th63c: Rseq is convergent_in_cod2 implies for Rseq1 be subsequence of Rseq holds Rseq1 is convergent_in_cod2

 proof

 assume

 a1: Rseq is convergent_in_cod2;

 hereby

 let Rseq1 be subsequence of Rseq;

 consider I1,I2 be increasing sequence of NAT such that

 a7: for n, m holds (Rseq1 . (n,m)) = (Rseq . ((I1 . n),(I2 . m))) by def9;

 for m be Element of NAT holds ( ProjMap1 (Rseq1,m)) is convergent

 proof

 let m be Element of NAT ;

 reconsider m1 = (I1 . m) as Element of NAT ;



 a4: ( ProjMap1 (Rseq,m1)) is convergent by a1;

 now

 let e;

 assume 0 < e;

 then

 consider N such that

 a5: for n st n >= N holds |.((( ProjMap1 (Rseq,m1)) . n) - ( lim ( ProjMap1 (Rseq,m1)))).| < e by a4, SEQ_2:def 7;

 take N;

 hereby

 let n;

 assume

 a6: n >= N;



 x2: n is Element of NAT & (I1 . m) is Element of NAT & (I2 . n) is Element of NAT by ORDINAL1:def 12;

 (I2 . n) >= n by lem01;

 then (I2 . n) >= N by a6, XXREAL_0: 2;

 then |.((( ProjMap1 (Rseq,m1)) . (I2 . n)) - ( lim ( ProjMap1 (Rseq,m1)))).| < e by a5;

 then |.((Rseq . ((I1 . m),(I2 . n))) - ( lim ( ProjMap1 (Rseq,m1)))).| < e by MESFUNC9:def 6;

 then |.((Rseq1 . (m,n)) - ( lim ( ProjMap1 (Rseq,m1)))).| < e by a7;

 hence |.((( ProjMap1 (Rseq1,m)) . n) - ( lim ( ProjMap1 (Rseq,m1)))).| < e by x2, MESFUNC9:def 6;

 end;

 end;

 hence ( ProjMap1 (Rseq1,m)) is convergent by SEQ_2:def 6;

 end;

 hence Rseq1 is convergent_in_cod2;

 end;

 end;

 registration

 let Rseq be convergent_in_cod2 Function of [: NAT , NAT :], REAL ;

 cluster -> convergent_in_cod2 for subsequence of Rseq;

 coherence by th63c;

 end

 theorem :: DBLSEQ_1:19

 for Rseq1 be subsequence of Rseq st Rseq is convergent_in_cod2 & ( lim_in_cod2 Rseq) is convergent holds ( lim_in_cod2 Rseq1) is convergent & ( cod2_major_iterated_lim Rseq1) = ( cod2_major_iterated_lim Rseq)

 proof

 let Rseq1 be subsequence of Rseq;

 assume that

 a1: Rseq is convergent_in_cod2 & ( lim_in_cod2 Rseq) is convergent;

 consider I1,I2 be increasing sequence of NAT such that

 a7: for n, m holds (Rseq1 . (n,m)) = (Rseq . ((I1 . n),(I2 . m))) by def9;



 a8: Rseq1 is convergent_in_cod2 by a1;



 a10: for e st 0 < e holds ex N st for m st m >= N holds |.((( lim_in_cod2 Rseq1) . m) - ( cod2_major_iterated_lim Rseq)).| < e

 proof

 let e;

 assume 0 < e;

 then

 consider N such that

 a11: for m st m >= N holds |.((( lim_in_cod2 Rseq) . m) - ( cod2_major_iterated_lim Rseq)).| < e by a1, def35;

 take N;

 hereby

 let m;

 reconsider mm = m as Element of NAT by ORDINAL1:def 12;

 assume

 a12: m >= N;

 reconsider m1 = (I1 . m) as Element of NAT ;



 x2: ( ProjMap1 (Rseq1,mm)) is convergent by a8;

 for p be Real st 0 = K holds |.((( ProjMap1 (Rseq1,mm)) . n) - ( lim ( ProjMap1 (Rseq,m1)))).| < p

 proof

 let p be Real;

 assume

 b1: 0 < p;

 ( ProjMap1 (Rseq,m1)) is convergent by a1;

 then

 consider K be Nat such that

 b2: for n st n >= K holds |.((( ProjMap1 (Rseq,m1)) . n) - ( lim ( ProjMap1 (Rseq,m1)))).| = K;



 x3: n is Element of NAT & (I1 . m) is Element of NAT & (I2 . n) is Element of NAT by ORDINAL1:def 12;

 (I2 . n) >= n by lem01;

 then (I2 . n) >= K by b3, XXREAL_0: 2;

 then |.((( ProjMap1 (Rseq,m1)) . (I2 . n)) - ( lim ( ProjMap1 (Rseq,m1)))).| < p by b2;

 then |.((Rseq . ((I1 . m),(I2 . n))) - ( lim ( ProjMap1 (Rseq,m1)))).| < p by MESFUNC9:def 6;

 then |.((Rseq1 . (m,n)) - ( lim ( ProjMap1 (Rseq,m1)))).| < p by a7;

 hence |.((( ProjMap1 (Rseq1,mm)) . n) - ( lim ( ProjMap1 (Rseq,m1)))).| = m by lem01;

 then (I1 . m) >= N by a12, XXREAL_0: 2;

 then

 a13: |.((( lim_in_cod2 Rseq) . (I1 . m)) - ( cod2_major_iterated_lim Rseq)).| < e by a11;

 (( lim_in_cod2 Rseq) . (I1 . m)) = ( lim ( ProjMap1 (Rseq,m1))) by def33;

 hence |.((( lim_in_cod2 Rseq1) . m) - ( cod2_major_iterated_lim Rseq)).| < e by def33, a13, c1;

 end;

 end;

 hence ( lim_in_cod2 Rseq1) is convergent by SEQ_2:def 6;

 hence thesis by a10, def35;

 end;