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