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