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

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

let i, j be Nat; :: thesis: ( i <= j implies (lim_in_cod1 Rseq) . i <= (lim_in_cod1 Rseq) . j )
assume a4: i <= j ; :: thesis: (lim_in_cod1 Rseq) . i <= (lim_in_cod1 Rseq) . j
reconsider n1 = i, n2 = j as Element of NAT by ORDINAL1:def 12;
a5: ( ProjMap2 (Rseq,n1) is convergent & ProjMap2 (Rseq,n2) is convergent ) by a2;

now :: thesis: for m being Nat holds (ProjMap2 (Rseq,n1)) . m <= (ProjMap2 (Rseq,n2)) . m

let m be Nat; :: thesis: (ProjMap2 (Rseq,n1)) . m <= (ProjMap2 (Rseq,n2)) . m
m in NAT by ORDINAL1:def 12;
then ( (ProjMap2 (Rseq,n1)) . m = Rseq . (m,n1) & (ProjMap2 (Rseq,n2)) . m = Rseq . (m,n2) ) by MESFUNC9:def 7;
hence (ProjMap2 (Rseq,n1)) . m <= (ProjMap2 (Rseq,n2)) . m by a1, a4; :: thesis: verum

end;

then lim (ProjMap2 (Rseq,n1)) <= lim (ProjMap2 (Rseq,n2)) by a5, SEQ_2:18;
then (lim_in_cod1 Rseq) . n1 <= lim (ProjMap2 (Rseq,n2)) by DBLSEQ_1:def 5;
hence (lim_in_cod1 Rseq) . i <= (lim_in_cod1 Rseq) . j by DBLSEQ_1:def 5; :: thesis: verum

end;

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