let n be Nat; :: thesis: for x, y being Element of REAL n holds |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)
let x, y be Element of REAL n; :: thesis: |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)
thus |.(x + y).| ^2 = |((x + y),(x + y))| by EUCLID_2:4
.= (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by Th37
.= ((|.x.| ^2) + (2 * |(x,y)|)) + |(y,y)| by EUCLID_2:4
.= ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2) by EUCLID_2:4 ; :: thesis: verum