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 Def13
.= (a * (y .|. x)) *' by Def13
.= (a *' ) * ((y .|. x) *' ) by COMPLEX1:121
.= (a *' ) * (x .|. y) by Def13 ; :: thesis: verum