theorem lm84: :: DBLSEQ_2:32

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st Rseq1 is nonnegative-yielding & ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds
for i, j being Nat holds (Partial_Sums Rseq1) . (i,j) <= (Partial_Sums Rseq2) . (i,j)