for seq1 being Real_Sequence
for n, m being Nat st n <= m & ( for i being Nat holds seq1 . i >= 0 ) holds
(Partial_Sums seq1) . n <= (Partial_Sums seq1) . m