let V be RealUnitarySpace; :: thesis: for x, y being VECTOR of V holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
let x, y be VECTOR of V; :: thesis: (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
(||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2)) + (||.(x - y).|| ^2) by Th29
.= (((||.x.|| ^2) + (2 * (x .|. y))) + (||.y.|| ^2)) + (((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2)) by Th29
.= ((||.x.|| ^2) + (||.x.|| ^2)) + (2 * (||.y.|| ^2)) ;
hence (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2)) ; :: thesis: verum