for X being RealUnitarySpace
for x, y being Point of X holds (x + y) .|. (x - y) = (x .|. x) - (y .|. y)