let n be Nat; :: thesis: for x, y being Element of REAL n holds (|.(x + y).| ^2 ) + (|.(x - y).| ^2 ) = 2 * ((|.x.| ^2 ) + (|.y.| ^2 ))
let x, y be Element of REAL n; :: thesis: (|.(x + y).| ^2 ) + (|.(x - y).| ^2 ) = 2 * ((|.x.| ^2 ) + (|.y.| ^2 ))
( len x = n & len y = n ) by FINSEQ_1:def 18;
hence (|.(x + y).| ^2 ) + (|.(x - y).| ^2 ) = 2 * ((|.x.| ^2 ) + (|.y.| ^2 )) by EUCLID_2:35; :: thesis: verum