theorem Th16: :: BHSP_1:16

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