let X be ComplexUnitarySpace; :: 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 A1: x,y are_orthogonal ; :: thesis: (x - y) .|. (x - y) = (x .|. x) + (y .|. y)
then A2: x .|. y = 0 by Def14;
(x - y) .|. (x - y) = (((x .|. x) - (x .|. y)) - (y .|. x)) + (y .|. y) by Th35
.= ((x .|. x) + (y .|. y)) - 0 by A1, A2, Def14 ;
hence (x - y) .|. (x - y) = (x .|. x) + (y .|. y) ; :: thesis: verum