theorem :: DBLSEQ_2:35

for Rseq being Function of [:NAT,NAT:],REAL st Rseq is nonnegative-yielding holds
for m, n being Nat holds
( Rseq . (m,n) <= (Partial_Sums_in_cod1 Rseq) . (m,n) & Rseq . (m,n) <= (Partial_Sums_in_cod2 Rseq) . (m,n) )