theorem :: DBLSEQ_3:88

for f being nonnegative Function of [:NAT,NAT:],ExtREAL holds
( ( for i1, i2, j being Nat st i1 <= i2 holds
(Partial_Sums_in_cod1 f) . (i1,j) <= (Partial_Sums_in_cod1 f) . (i2,j) ) & ( for i, j1, j2 being Nat st j1 <= j2 holds
(Partial_Sums_in_cod2 f) . (i,j1) <= (Partial_Sums_in_cod2 f) . (i,j2) ) )