theorem :: BHSP_1:3

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