for V being RealUnitarySpace
for x, y being VECTOR of V holds
( ||.(x + y).|| ^2 = ((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2) & ||.(x - y).|| ^2 = ((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2) )