let V be RealUnitarySpace; :: thesis: for x, y being VECTOR of V holds
( ||.(x + y).|| ^2 = ((||.x.|| ^2 ) + (2 * (x .|. y))) + (||.y.|| ^2 ) & ||.(x - y).|| ^2 = ((||.x.|| ^2 ) - (2 * (x .|. y))) + (||.y.|| ^2 ) )
let x, y be VECTOR of V; :: thesis: ( ||.(x + y).|| ^2 = ((||.x.|| ^2 ) + (2 * (x .|. y))) + (||.y.|| ^2 ) & ||.(x - y).|| ^2 = ((||.x.|| ^2 ) - (2 * (x .|. y))) + (||.y.|| ^2 ) )
A1: x .|. x >= 0 by BHSP_1:def 2;
||.(x + y).|| = sqrt ((x + y) .|. (x + y)) by BHSP_1:def 4;
then A2: sqrt (||.(x + y).|| ^2 ) = sqrt ((x + y) .|. (x + y)) by BHSP_1:34, SQUARE_1:89;
A3: y .|. y >= 0 by BHSP_1:def 2;
( (x + y) .|. (x + y) >= 0 & ||.(x + y).|| ^2 >= 0 ) by BHSP_1:def 2, XREAL_1:65;
then ||.(x + y).|| ^2 = (x + y) .|. (x + y) by A2, SQUARE_1:96
.= ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:21
.= (((sqrt (x .|. x)) ^2 ) + (2 * (x .|. y))) + (y .|. y) by A1, SQUARE_1:def 4
.= ((||.x.|| ^2 ) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:def 4
.= ((||.x.|| ^2 ) + (2 * (x .|. y))) + ((sqrt (y .|. y)) ^2 ) by A3, SQUARE_1:def 4 ;
hence ||.(x + y).|| ^2 = ((||.x.|| ^2 ) + (2 * (x .|. y))) + (||.y.|| ^2 ) by BHSP_1:def 4; :: thesis: ||.(x - y).|| ^2 = ((||.x.|| ^2 ) - (2 * (x .|. y))) + (||.y.|| ^2 )
||.(x - y).|| = sqrt ((x - y) .|. (x - y)) by BHSP_1:def 4;
then A4: sqrt (||.(x - y).|| ^2 ) = sqrt ((x - y) .|. (x - y)) by BHSP_1:34, SQUARE_1:89;
( (x - y) .|. (x - y) >= 0 & ||.(x - y).|| ^2 >= 0 ) by BHSP_1:def 2, XREAL_1:65;
then ||.(x - y).|| ^2 = (x - y) .|. (x - y) by A4, SQUARE_1:96
.= ((x .|. x) - (2 * (x .|. y))) + (y .|. y) by BHSP_1:23
.= (((sqrt (x .|. x)) ^2 ) - (2 * (x .|. y))) + (y .|. y) by A1, SQUARE_1:def 4
.= ((||.x.|| ^2 ) - (2 * (x .|. y))) + (y .|. y) by BHSP_1:def 4
.= ((||.x.|| ^2 ) - (2 * (x .|. y))) + ((sqrt (y .|. y)) ^2 ) by A3, SQUARE_1:def 4 ;
hence ||.(x - y).|| ^2 = ((||.x.|| ^2 ) - (2 * (x .|. y))) + (||.y.|| ^2 ) by BHSP_1:def 4; :: thesis: verum