theorem lm84a: :: DBLSEQ_2:31

for Rseq1, Rseq2 being Function of [:NAT,NAT:],REAL st ( for n, m being Nat holds Rseq1 . (n,m) <= Rseq2 . (n,m) ) holds
for i, j being Nat holds
( (Partial_Sums_in_cod1 Rseq1) . (i,j) <= (Partial_Sums_in_cod1 Rseq2) . (i,j) & (Partial_Sums_in_cod2 Rseq1) . (i,j) <= (Partial_Sums_in_cod2 Rseq2) . (i,j) )