:: deftheorem Def12 defines are_orthogonal CSSPACE:def 14 :
for X being ComplexUnitarySpace
for x, y being Point of X holds
( x,y are_orthogonal iff x .|. y = 0 );