for a being Real
for X being RealUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. (a * y)