let X be RealUnitarySpace; :: thesis: for x, y being Point of X holds (||.(x + y).|| * ||.(x + y).||) + (||.(x - y).|| * ||.(x - y).||) = (2 * (||.x.|| * ||.x.||)) + (2 * (||.y.|| * ||.y.||))
let x, y be Point of X; :: thesis: (||.(x + y).|| * ||.(x + y).||) + (||.(x - y).|| * ||.(x - y).||) = (2 * (||.x.|| * ||.x.||)) + (2 * (||.y.|| * ||.y.||))
( ||.(x + y).|| ^2 = ||.(x + y).|| * ||.(x + y).|| & ||.(x - y).|| ^2 = ||.(x - y).|| * ||.(x - y).|| & ||.x.|| ^2 = ||.x.|| * ||.x.|| & ||.y.|| ^2 = ||.y.|| * ||.y.|| ) by SQUARE_1:def 1;
hence (||.(x + y).|| * ||.(x + y).||) + (||.(x - y).|| * ||.(x - y).||) = (2 * (||.x.|| * ||.x.||)) + (2 * (||.y.|| * ||.y.||)) by RUSUB_5:31; :: thesis: verum