let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds (- x) .|. y = x .|. (- y)
let x, y be Point of X; :: thesis: (- x) .|. y = x .|. (- y)
(- x) .|. y = ((- 1r) * x) .|. y by CLVECT_1:3
.= x .|. (((- 1r) *') * y) by Th14
.= x .|. ((- 1r) * y) by COMPLEX1:30, COMPLEX1:33 ;
hence (- x) .|. y = x .|. (- y) by CLVECT_1:3; :: thesis: verum