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