for seq being Real_Sequence
for k being Nat holds |.((Partial_Sums seq) . k).| <= (Partial_Sums (abs seq)) . k