theorem :: BHSP_1:2

for X being RealUnitarySpace
for x, y, z being Point of X holds x .|. (y + z) = (x .|. y) + (x .|. z) by Def2;