let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is non-decreasing implies ( ( for m being Element of NAT holds ProjMap1 (Rseq,m) is non-decreasing ) & ( for n being Element of NAT holds ProjMap2 (Rseq,n) is non-decreasing ) ) )
assume a1: Rseq is non-decreasing ; :: thesis: ( ( for m being Element of NAT holds ProjMap1 (Rseq,m) is non-decreasing ) & ( for n being Element of NAT holds ProjMap2 (Rseq,n) is non-decreasing ) )

hereby :: thesis: for n being Element of NAT holds ProjMap2 (Rseq,n) is non-decreasing

let m be Element of NAT ; :: thesis: ProjMap1 (Rseq,m) is non-decreasing

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

let n1, n2 be Nat; :: thesis: ( n1 <= n2 implies (ProjMap1 (Rseq,m)) . n1 <= (ProjMap1 (Rseq,m)) . n2 )
a0: ( n1 in NAT & n2 in NAT ) by ORDINAL1:def 12;
assume n1 <= n2 ; :: thesis: (ProjMap1 (Rseq,m)) . n1 <= (ProjMap1 (Rseq,m)) . n2
then Rseq . (m,n1) <= Rseq . (m,n2) by a1;
then (ProjMap1 (Rseq,m)) . n1 <= Rseq . (m,n2) by a0, MESFUNC9:def 6;
hence (ProjMap1 (Rseq,m)) . n1 <= (ProjMap1 (Rseq,m)) . n2 by a0, MESFUNC9:def 6; :: thesis: verum

end;

hence ProjMap1 (Rseq,m) is non-decreasing by SEQM_3:6; :: thesis: verum

end;

hereby :: thesis: verum

let m be Element of NAT ; :: thesis: ProjMap2 (Rseq,m) is non-decreasing

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

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

end;

hence ProjMap2 (Rseq,m) is non-decreasing by SEQM_3:6; :: thesis: verum

end;