theorem LOPBAN410: :: LOPBAN13:1

for X being RealNormSpace
for seq being sequence of X
for k being Nat holds ||.((Partial_Sums seq) . k).|| <= (Partial_Sums ||.seq.||) . k