let X be RealUnitarySpace; :: thesis: for x, y being Point of X holds (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
let x, y be Point of X; :: thesis: (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2))
A1: (x + y) .|. (x + y) >= 0 by BHSP_1:def 2;
A2: (x - y) .|. (x - y) >= 0 by BHSP_1:def 2;
A3: x .|. x >= 0 by BHSP_1:def 2;
A4: y .|. y >= 0 by BHSP_1:def 2;
(||.(x + y).|| ^2) + (||.(x - y).|| ^2) = ((sqrt ((x + y) .|. (x + y))) ^2) + (||.(x - y).|| ^2) by BHSP_1:def 4
.= ((x + y) .|. (x + y)) + (||.(x - y).|| ^2) by A1, SQUARE_1:def 2
.= ((x + y) .|. (x + y)) + ((sqrt ((x - y) .|. (x - y))) ^2) by BHSP_1:def 4
.= ((x + y) .|. (x + y)) + ((x - y) .|. (x - y)) by A2, SQUARE_1:def 2
.= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + ((x - y) .|. (x - y)) by BHSP_1:16
.= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + (((x .|. x) - (2 * (x .|. y))) + (y .|. y)) by BHSP_1:18
.= (2 * (x .|. x)) + (2 * (y .|. y))
.= (2 * ((sqrt (x .|. x)) ^2)) + (2 * (y .|. y)) by A3, SQUARE_1:def 2
.= (2 * ((sqrt (x .|. x)) ^2)) + (2 * ((sqrt (y .|. y)) ^2)) by A4, SQUARE_1:def 2
.= (2 * (||.x.|| ^2)) + (2 * ((sqrt (y .|. y)) ^2)) by BHSP_1:def 4
.= (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2)) by BHSP_1:def 4 ;
hence (||.(x + y).|| ^2) + (||.(x - y).|| ^2) = (2 * (||.x.|| ^2)) + (2 * (||.y.|| ^2)) ; :: thesis: verum