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:28, SQUARE_1:22;
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:63;
then ||.(x + y).|| ^2 = (x + y) .|. (x + y) by A2, SQUARE_1:28
.= ((x .|. x) + (2 * (x .|. y))) + (y .|. y) by BHSP_1:16
.= (((sqrt (x .|. x)) ^2) + (2 * (x .|. y))) + (y .|. y) by A1, SQUARE_1:def 2
.= ((||.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 2 ;
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:28, SQUARE_1:22;
( (x - y) .|. (x - y) >= 0 & ||.(x - y).|| ^2 >= 0 ) by BHSP_1:def 2, XREAL_1:63;
then ||.(x - y).|| ^2 = (x - y) .|. (x - y) by A4, SQUARE_1:28
.= ((x .|. x) - (2 * (x .|. y))) + (y .|. y) by BHSP_1:18
.= (((sqrt (x .|. x)) ^2) - (2 * (x .|. y))) + (y .|. y) by A1, SQUARE_1:def 2
.= ((||.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 2 ;
hence ||.(x - y).|| ^2 = ((||.x.|| ^2) - (2 * (x .|. y))) + (||.y.|| ^2) by BHSP_1:def 4; :: thesis: verum