for X being ComplexUnitarySpace
for x being Point of X holds |.(x .|. x).| = Re (x .|. x)