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 + y).|| = sqrt ((x + y) .|. (x + y)) by BHSP_1:def 4;
A2: (x + y) .|. (x + y) >= 0 by BHSP_1:def 2;
A3: ||.(x + y).|| ^2 >= 0 by XREAL_1:65;
A4: x .|. x >= 0 by BHSP_1:def 2;
A5: y .|. y >= 0 by BHSP_1:def 2;
sqrt (||.(x + y).|| ^2 ) = sqrt ((x + y) .|. (x + y)) by A1, BHSP_1:34, SQUARE_1:89;
then ||.(x + y).|| ^2 = (x + y) .|. (x + y) by A2, A3, SQUARE_1:96
.= ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:21
.= (((sqrt (x .|. x)) ^2 ) + (2 * (x .|. y))) + (y .|. y) by A4, 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 A5, 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 )
A6: ||.(x - y).|| = sqrt ((x - y) .|. (x - y)) by BHSP_1:def 4;
A7: (x - y) .|. (x - y) >= 0 by BHSP_1:def 2;
A8: ||.(x - y).|| ^2 >= 0 by XREAL_1:65;
sqrt (||.(x - y).|| ^2 ) = sqrt ((x - y) .|. (x - y)) by A6, BHSP_1:34, SQUARE_1:89;
then ||.(x - y).|| ^2 = (x - y) .|. (x - y) by A7, A8, SQUARE_1:96
.= ((x .|. x) - (2 * (x .|. y))) + (y .|. y) by BHSP_1:23
.= (((sqrt (x .|. x)) ^2 ) - (2 * (x .|. y))) + (y .|. y) by A4, 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 A5, SQUARE_1:def 4 ;
hence ||.(x - y).|| ^2 = ((||.x.|| ^2 ) - (2 * (x .|. y))) + (||.y.|| ^2 ) by BHSP_1:def 4; :: thesis: verum