let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( Rseq is nonnegative-yielding implies Partial_Sums Rseq is non-decreasing )
set CPS = Partial_Sums Rseq;
assume a1: Rseq is nonnegative-yielding ; :: thesis: Partial_Sums Rseq is non-decreasing

now :: thesis: for n1, m1, n2, m2 being Nat st n1 >= n2 & m1 >= m2 holds
(Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2)

let n1, m1, n2, m2 be Nat; :: thesis: ( n1 >= n2 & m1 >= m2 implies (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2) )
assume b2: ( n1 >= n2 & m1 >= m2 ) ; :: thesis: (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2)
then consider dn being Nat such that
b3: n1 = n2 + dn by NAT_1:10;
consider dm being Nat such that
b4: m1 = m2 + dm by b2, NAT_1:10;
reconsider dn = dn, dm = dm as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat] means (Partial_Sums Rseq) . ((n2 + $1),m2) >= (Partial_Sums Rseq) . (n2,m2);
b5: S₁[ 0 ] ;
b6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume a7: S₁[k] ; :: thesis: S₁[k + 1]
b8: (Partial_Sums Rseq) . (((n2 + k) + 1),m2) = ((Partial_Sums_in_cod2 Rseq) . (((n2 + k) + 1),m2)) + ((Partial_Sums Rseq) . ((n2 + k),m2)) by ThRS;
Partial_Sums_in_cod2 Rseq is nonnegative-yielding by a1, lm80;
then (Partial_Sums Rseq) . (((n2 + k) + 1),m2) >= (Partial_Sums Rseq) . ((n2 + k),m2) by b8, XREAL_1:31;
hence S₁[k + 1] by a7, XXREAL_0:2; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(b5, b6);
then b9: (Partial_Sums Rseq) . (n1,m2) >= (Partial_Sums Rseq) . (n2,m2) by b3;
defpred S₂[ Nat] means (Partial_Sums Rseq) . (n1,(m2 + $1)) >= (Partial_Sums Rseq) . (n1,m2);
b10: S₂[ 0 ] ;
b11: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume b12: S₂[k] ; :: thesis: S₂[k + 1]
b13: (Partial_Sums Rseq) . (n1,((m2 + k) + 1)) = ((Partial_Sums_in_cod1 Rseq) . (n1,((m2 + k) + 1))) + ((Partial_Sums Rseq) . (n1,(m2 + k))) by DefCS;
Partial_Sums_in_cod1 Rseq is nonnegative-yielding by a1, lm80;
then (Partial_Sums Rseq) . (n1,((m2 + k) + 1)) >= (Partial_Sums Rseq) . (n1,(m2 + k)) by b13, XREAL_1:31;
hence S₂[k + 1] by b12, XXREAL_0:2; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(b10, b11);
then (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n1,m2) by b4;
hence (Partial_Sums Rseq) . (n1,m1) >= (Partial_Sums Rseq) . (n2,m2) by b9, XXREAL_0:2; :: thesis: verum

end;

hence Partial_Sums Rseq is non-decreasing ; :: thesis: verum