let a be Complex; :: thesis: for X being ComplexUnitarySpace
for x, y being Point of X holds (a * x) .|. y = x .|. ((a *') * y)
let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds (a * x) .|. y = x .|. ((a *') * y)
let x, y be Point of X; :: thesis: (a * x) .|. y = x .|. ((a *') * y)
(a * x) .|. y = a * (x .|. y) by Def13
.= ((a *') *') * ((y .|. x) *') by Def13
.= ((a *') * (y .|. x)) *' by COMPLEX1:35
.= (((a *') * y) .|. x) *' by Def13 ;
hence (a * x) .|. y = x .|. ((a *') * y) by Def13; :: thesis: verum