theorem th101: :: DBLSEQ_2:34

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