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