theorem Th45: :: CSSPACE:50

for X being ComplexUnitarySpace
for x being Point of X holds dist (x,x) = 0