for V being RealUnitarySpace
for x, y being VECTOR of V st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2) + (||.y.|| ^2)