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:4
.= x .|. (((- 1r ) *' ) * y) by Th21
.= x .|. ((- 1r ) * y) by COMPLEX1:115, COMPLEX1:119 ;
hence (- x) .|. y = x .|. (- y) by CLVECT_1:4; :: thesis: verum