let X be RealUnitarySpace; :: thesis: for x, y being Point of X st x,y are_orthogonal holds
(x - y) .|. (x - y) = (x .|. x) + (y .|. y)
let x, y be Point of X; :: thesis: ( x,y are_orthogonal implies (x - y) .|. (x - y) = (x .|. x) + (y .|. y) )
assume x,y are_orthogonal ; :: thesis: (x - y) .|. (x - y) = (x .|. x) + (y .|. y)
then A1: x .|. y = 0 ;
(x - y) .|. (x - y) = ((x .|. x) - (2 * (x .|. y))) + (y .|. y) by Th18
.= ((x .|. x) + (y .|. y)) - 0 by A1 ;
hence (x - y) .|. (x - y) = (x .|. x) + (y .|. y) ; :: thesis: verum