theorem Th2: :: CLOPBAN3:2

for X being ComplexNormSpace
for seq being sequence of X
for m being Nat holds 0 <= ||.seq.|| . m