Description: Conjugate law for inner product. Postulate (S1) of Beran p. 95. Note
that *x is the complex conjugate cjval of x . In the
literature, the inner product of A and B is usually written
<. A , B >. , but our operation notation co allows us to use
existing theorems about operations and also avoids a clash with the
definition of an ordered pair df-op . Physicists use <. B | A >. ,
called Dirac bra-ket notation, to represent this operation; see comments
in df-bra . (Contributed by NM, 29-Jul-1999)(New usage is discouraged.)