theorem :: DBLSEQ_3:5

for seq being nonpositive ExtREAL_sequence
for m being Nat holds seq . m >= (Partial_Sums seq) . m