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
.= (- 1) * (x .|. y) by Def13, COMPLEX1:def 7 ;
hence (- x) .|. y = - (x .|. y) ; :: thesis: verum