for rseq1, rseq2 being Real_Sequence
for m being Nat
for p being Real st ( for n being Nat st n <= m holds
rseq1 . n <= p * (rseq2 . n) ) holds
(Partial_Sums rseq1) . m <= p * ((Partial_Sums rseq2) . m)