let X be ComplexUnitarySpace; :: thesis: for x, y, z being Point of X holds (x - y) .|. z = (x .|. z) - (y .|. z)
let x, y, z be Point of X; :: thesis: (x - y) .|. z = (x .|. z) - (y .|. z)
(x - y) .|. z = (x .|. z) + ((- y) .|. z) by Def11
.= (x .|. z) + (- (y .|. z)) by Th18 ;
hence (x - y) .|. z = (x .|. z) - (y .|. z) ; :: thesis: verum