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:12
.= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| by Th38
.= ((|.x.| ^2 ) - (2 * |(x,y)|)) + |(y,y)| by EUCLID_2:12
.= ((|.x.| ^2 ) - (2 * |(x,y)|)) + (|.y.| ^2 ) by EUCLID_2:12 ; :: thesis: verum