theorem :: CLVECT_3:36

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