let X be RealUnitarySpace; :: thesis: for x, y being Point of X holds (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)
let x, y be Point of X; :: thesis: (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y)
(x - y) .|. (x - y) = (x .|. (x - y)) - (y .|. (x - y)) by Th11
.= ((x .|. x) - (x .|. y)) - (y .|. (x - y)) by Th12
.= ((x .|. x) - (x .|. y)) - ((x .|. y) - (y .|. y)) by Th12
.= ((x .|. x) - ((x .|. y) + (x .|. y))) + (y .|. y) ;
hence (x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y) ; :: thesis: verum