theorem Th12: :: NAGATA_2:12

for r being Real
for n being Nat
for seq being Real_Sequence st ( for m being Nat st m <= n holds
seq . m <= r ) holds
for m being Nat st m <= n holds
(Partial_Sums seq) . m <= r * (m + 1)