Real means :def35:
for e be Real st 0

0
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;
attr Rseq is uniformly_convergent_in_cod2 means
Rseq is convergent_in_cod2 &
for e be Real st e>0
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;
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);
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 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

=K holds |.ProjMap2(Rseq1,m1).n - lim ProjMap2(Rseq,m2).| < p proof let p be Real; assume b1: 0

=K holds |.ProjMap2(Rseq,m2).n - lim ProjMap2(Rseq,m2).| < p by b1,SEQ_2:def 7; take K; hereby let n; assume b3: n >= 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).|

= 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

=K holds |.ProjMap1(Rseq1,mm).n - lim ProjMap1(Rseq,m1).| < p proof let p be Real; assume b1: 0

=K holds |. ProjMap1(Rseq,m1).n - lim ProjMap1(Rseq,m1).| < p by b1,SEQ_2:def 7; take K; hereby let n; assume b3: n >= 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).|

= 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;