theorem Th105: :: CLVECT_1:105

for CNS being ComplexNormSpace
for x being Point of CNS holds 0 <= ||.x.||