theorem th1003: :: DBLSEQ_2:36

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_in_cod1 Rseq) . (i1,j) <= (Partial_Sums_in_cod1 Rseq) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 Rseq) . (i,j1) <= (Partial_Sums_in_cod2 Rseq) . (i,j2) ) )