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