for rseq being Real_Sequence
for p being Real st ( for n being Nat holds rseq . n <= p ) holds
for n, l being Nat holds ((Partial_Sums rseq) . (n + l)) - ((Partial_Sums rseq) . n) <= p * l