for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums Rseq) . (i1,j) <= (Partial_Sums Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums Rseq) . (i,j1) <= (Partial_Sums Rseq) . (i,j2) ) )