theorem Th13: :: NAGATA_2:13

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