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