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