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