theorem Th4: :: DBLSEQ_3:4

for seq being nonnegative ExtREAL_sequence
for m being Nat holds seq . m <= (Partial_Sums seq) . m