theorem :: BHSP_1:6

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