let V be RealUnitarySpace; :: thesis: for x, y being VECTOR of V st x,y are_orthogonal holds
||.(x + y).|| ^2 = (||.x.|| ^2 ) + (||.y.|| ^2 )
let x, y be VECTOR of V; :: thesis: ( x,y are_orthogonal implies ||.(x + y).|| ^2 = (||.x.|| ^2 ) + (||.y.|| ^2 ) )
assume x,y are_orthogonal ; :: thesis: ||.(x + y).|| ^2 = (||.x.|| ^2 ) + (||.y.|| ^2 )
then A1: x .|. y = 0 by BHSP_1:def 3;
||.(x + y).|| ^2 = ((||.x.|| ^2 ) + (2 * (x .|. y))) + (||.y.|| ^2 ) by Th29;
hence ||.(x + y).|| ^2 = (||.x.|| ^2 ) + (||.y.|| ^2 ) by A1; :: thesis: verum