for rseq being Real_Sequence
for m being Nat st rseq is nonnegative holds
rseq . m <= (Partial_Sums rseq) . m