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