for a being Complex
for X being ComplexUnitarySpace
for x, y being Point of X holds x .|. (a * y) = (a *') * (x .|. y)