let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is non-increasing & Rseq is bounded_below implies ( Rseq is P-convergent & Rseq is convergent_in_cod1 & Rseq is convergent_in_cod2 ) )
assume that
a1: Rseq is non-increasing and
a2: Rseq is bounded_below ; :: thesis: ( Rseq is P-convergent & Rseq is convergent_in_cod1 & Rseq is convergent_in_cod2 )
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 being Real st 0 < e holds
ex N being Nat st Rseq . (N,N) < M + e

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st Rseq . (N,N) < M + e )
assume a4: 0 < e ; :: thesis: ex N being Nat st Rseq . (N,N) < M + e
assume a7: for n being Nat holds Rseq . (n,n) >= M + e ; :: thesis: contradiction

now :: thesis: for a being ExtReal st a in Rseq .: [:NAT,NAT:] holds
a >= M + e

let a be ExtReal; :: thesis: ( a in Rseq .: [:NAT,NAT:] implies a >= M + e )
assume a in Rseq .: [:NAT,NAT:] ; :: thesis: a >= M + e
then consider x being object such that
a5: ( x in dom Rseq & a = Rseq . x ) by b3, FUNCT_1:def 3;
consider i, j being object such that
a6: ( i in NAT & j in NAT & x = [i,j] ) by a5, ZFMISC_1:def 2;
reconsider i = i, j = 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; :: thesis: verum

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; :: thesis: verum

end;

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

proof

let e be Real; :: thesis: ( 0 < e implies ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - M).| < e )
assume a5: 0 < e ; :: thesis: ex N being Nat st
for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - M).| < e
then consider N being Nat such that
a10: Rseq . (N,N) < M + e by a3;
take N ; :: thesis: for n, m being Nat st n >= N & m >= N holds
|.((Rseq . (n,m)) - M).| < e

hereby :: thesis: verum

let n, m be Nat; :: thesis: ( n >= N & m >= N implies |.((Rseq . (n,m)) - M).| < e )
assume ( n >= N & m >= N ) ; :: thesis: |.((Rseq . (n,m)) - M).| < e
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; :: thesis: verum

end;

end;

hence Rseq is P-convergent ; :: thesis: ( Rseq is convergent_in_cod1 & Rseq is convergent_in_cod2 )
for m being Element of NAT holds ProjMap2 (Rseq,m) is convergent

proof

let m be Element of NAT ; :: thesis: ProjMap2 (Rseq,m) is convergent
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 :: thesis: for a being object st a in (ProjMap2 (Rseq,m)) .: NAT holds
a in Rseq .: [:NAT,NAT:]

let a be object ; :: thesis: ( a in (ProjMap2 (Rseq,m)) .: NAT implies a in Rseq .: [:NAT,NAT:] )
assume a in (ProjMap2 (Rseq,m)) .: NAT ; :: thesis: a in Rseq .: [:NAT,NAT:]
then consider i being object such that
c4: ( i in dom (ProjMap2 (Rseq,m)) & a = (ProjMap2 (Rseq,m)) . i ) by c3, FUNCT_1:def 3;
reconsider i = 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; :: thesis: verum

end;

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

now :: thesis: for n being Nat holds (ProjMap2 (Rseq,m)) . n >= (ProjMap2 (Rseq,m)) . (n + 1)

let n be Nat; :: thesis: (ProjMap2 (Rseq,m)) . n >= (ProjMap2 (Rseq,m)) . (n + 1)
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; :: thesis: verum

end;

then ProjMap2 (Rseq,m) is non-increasing by SEQM_3:def 9;
hence ProjMap2 (Rseq,m) is convergent by c5; :: thesis: verum

end;

hence Rseq is convergent_in_cod1 ; :: thesis: Rseq is convergent_in_cod2
for m being Element of NAT holds ProjMap1 (Rseq,m) is convergent

proof

let m be Element of NAT ; :: thesis: ProjMap1 (Rseq,m) is convergent
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 :: thesis: for a being object st a in (ProjMap1 (Rseq,m)) .: NAT holds
a in Rseq .: [:NAT,NAT:]

let a be object ; :: thesis: ( a in (ProjMap1 (Rseq,m)) .: NAT implies a in Rseq .: [:NAT,NAT:] )
assume a in (ProjMap1 (Rseq,m)) .: NAT ; :: thesis: a in Rseq .: [:NAT,NAT:]
then consider i being object such that
c4: ( i in dom (ProjMap1 (Rseq,m)) & a = (ProjMap1 (Rseq,m)) . i ) by c3, FUNCT_1:def 3;
reconsider i = 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; :: thesis: verum

end;

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

now :: thesis: for n being Nat holds (ProjMap1 (Rseq,m)) . n >= (ProjMap1 (Rseq,m)) . (n + 1)

let n be Nat; :: thesis: (ProjMap1 (Rseq,m)) . n >= (ProjMap1 (Rseq,m)) . (n + 1)
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; :: thesis: verum

end;

then ProjMap1 (Rseq,m) is non-increasing by SEQM_3:def 9;
hence ProjMap1 (Rseq,m) is convergent by c5; :: thesis: verum

end;

hence Rseq is convergent_in_cod2 ; :: thesis: verum