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