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 4
.= ((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 4
.= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + ((x - y) .|. (x - y)) by BHSP_1:21
.= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) + (((x .|. x) - (2 * (x .|. y))) + (y .|. y)) by BHSP_1:23
.= (2 * (x .|. x)) + (2 * (y .|. y))
.= (2 * ((sqrt (x .|. x)) ^2 )) + (2 * (y .|. y)) by A3, SQUARE_1:def 4
.= (2 * ((sqrt (x .|. x)) ^2 )) + (2 * ((sqrt (y .|. y)) ^2 )) by A4, SQUARE_1:def 4
.= (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