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