theorem Th5: :: BHSP_1:5

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