theorem Th39: :: CSSPACE:44

for X being ComplexUnitarySpace
for x being Point of X holds 0 <= ||.x.||