for n being Nat
for s being Real_Sequence holds (Partial_Sums s) . n <= (Partial_Sums (abs s)) . n