let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is non-decreasing & Rseq is convergent_in_cod2 implies lim_in_cod2 Rseq is non-decreasing )
assume that
a1: Rseq is non-decreasing and
a2: Rseq is convergent_in_cod2 ; :: thesis: lim_in_cod2 Rseq is non-decreasing

now :: thesis: for i, j being Nat st i <= j holds
(lim_in_cod2 Rseq) . i <= (lim_in_cod2 Rseq) . j

let i, j be Nat; :: thesis: ( i <= j implies (lim_in_cod2 Rseq) . i <= (lim_in_cod2 Rseq) . j )
assume a4: i <= j ; :: thesis: (lim_in_cod2 Rseq) . i <= (lim_in_cod2 Rseq) . j
reconsider m1 = i, m2 = j as Element of NAT by ORDINAL1:def 12;
p1: ( ProjMap1 (Rseq,m1) is convergent & ProjMap1 (Rseq,m2) is convergent ) by a2;

now :: thesis: for n being Nat holds (ProjMap1 (Rseq,m1)) . n <= (ProjMap1 (Rseq,m2)) . n

let n be Nat; :: thesis: (ProjMap1 (Rseq,m1)) . n <= (ProjMap1 (Rseq,m2)) . n
n in NAT by ORDINAL1:def 12;
then ( (ProjMap1 (Rseq,m1)) . n = Rseq . (m1,n) & (ProjMap1 (Rseq,m2)) . n = Rseq . (m2,n) ) by MESFUNC9:def 6;
hence (ProjMap1 (Rseq,m1)) . n <= (ProjMap1 (Rseq,m2)) . n by a1, a4; :: thesis: verum

end;

then lim (ProjMap1 (Rseq,m1)) <= lim (ProjMap1 (Rseq,m2)) by p1, SEQ_2:18;
then (lim_in_cod2 Rseq) . m1 <= lim (ProjMap1 (Rseq,m2)) by DBLSEQ_1:def 6;
hence (lim_in_cod2 Rseq) . i <= (lim_in_cod2 Rseq) . j by DBLSEQ_1:def 6; :: thesis: verum

end;

hence lim_in_cod2 Rseq is non-decreasing by SEQM_3:6; :: thesis: verum