for X being ComplexUnitarySpace
for x, y being Point of X st x,y are_orthogonal holds
(x + y) .|. (x + y) = (x .|. x) + (y .|. y)