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 = 0c by Def14;
y .|. x = 0c by A1, Def14;
then (x + y) .|. (x + y) = ((x .|. x) + 0c ) + (y .|. y) by A2, Th33;
hence (x + y) .|. (x + y) = (x .|. x) + (y .|. y) ; :: thesis: verum