theorem Th37: :: CLVECT_3:37

for X being ComplexUnitarySpace
for seq being sequence of X
for n being Nat holds ||.((Partial_Sums seq) . n).|| <= (Partial_Sums ||.seq.||) . n