let n be Nat; :: thesis: for y1, y2 being FinSequence of REAL
for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds
|(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 ))
let y1, y2 be FinSequence of REAL ; :: thesis: for x1, x2 being Element of REAL n st x1 = y1 & x2 = y2 holds
|(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 ))
let x1, x2 be Element of REAL n; :: thesis: ( x1 = y1 & x2 = y2 implies |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 )) )
assume A1: ( x1 = y1 & x2 = y2 ) ; :: thesis: |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 ))
set z1 = x1 + x2;
set z2 = x1 - x2;
A2: (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 )) = (1 / 4) * (((sqrt (Sum (sqr (x1 + x2)))) ^2 ) - (|.(x1 - x2).| ^2 )) by EUCLID:def 5
.= (1 / 4) * (((sqrt (Sum (sqr (x1 + x2)))) ^2 ) - ((sqrt (Sum (sqr (x1 - x2)))) ^2 )) by EUCLID:def 5 ;
Sum (sqr (x1 + x2)) >= 0 by RVSUM_1:116;
then A3: (sqrt (Sum (sqr (x1 + x2)))) ^2 = Sum (sqr (x1 + x2)) by SQUARE_1:def 4;
Sum (sqr (x1 - x2)) >= 0 by RVSUM_1:116;
then A4: (sqrt (Sum (sqr (x1 - x2)))) ^2 = Sum (sqr (x1 - x2)) by SQUARE_1:def 4;
set v1 = sqr (x1 + x2);
set v2 = sqr (x1 - x2);
reconsider w1 = x1, w2 = x2 as Element of n -tuples_on REAL by EUCLID:def 1;
A5: (Sum (sqr (x1 + x2))) - (Sum (sqr (x1 - x2))) = Sum ((sqr (x1 + x2)) - (sqr (x1 - x2))) by RVSUM_1:120;
A6: ((2 * (mlt w1,w2)) + (sqr w2)) + (2 * (mlt w1,w2)) = (2 * (mlt w1,w2)) + ((2 * (mlt w1,w2)) + (sqr w2))
.= ((2 * (mlt w1,w2)) + (2 * (mlt w1,w2))) + (sqr w2) by FINSEQOP:29 ;
A7: (sqr w1) + ((2 * (mlt w1,w2)) + (sqr w2)) = ((2 * (mlt w1,w2)) + (sqr w2)) + (sqr w1) ;
(sqr (x1 + x2)) - (sqr (x1 - x2)) = (((sqr w1) + (2 * (mlt w1,w2))) + (sqr w2)) - (sqr (w1 - w2)) by RVSUM_1:98
.= (((sqr w1) + (2 * (mlt w1,w2))) + (sqr w2)) - (((sqr w1) - (2 * (mlt w1,w2))) + (sqr w2)) by RVSUM_1:99
.= (((2 * (mlt w1,w2)) + (sqr w2)) + (sqr w1)) - (((sqr w1) - (2 * (mlt w1,w2))) + (sqr w2)) by A7, FINSEQOP:29
.= ((((2 * (mlt w1,w2)) + (sqr w2)) + (sqr w1)) - ((sqr w1) - (2 * (mlt w1,w2)))) - (sqr w2) by RVSUM_1:60
.= (((((2 * (mlt w1,w2)) + (sqr w2)) + (sqr w1)) - (sqr w1)) + (2 * (mlt w1,w2))) - (sqr w2) by RVSUM_1:62
.= (((2 * (mlt w1,w2)) + (sqr w2)) + (2 * (mlt w1,w2))) - (sqr w2) by RVSUM_1:63
.= (2 * (mlt w1,w2)) + (2 * (mlt w1,w2)) by A6, RVSUM_1:63
.= (2 + 2) * (mlt w1,w2) by RVSUM_1:72
.= 4 * (mlt w1,w2) ;
then (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 )) = (1 / 4) * (4 * (Sum (mlt w1,w2))) by A2, A3, A4, A5, RVSUM_1:117
.= Sum (mlt w1,w2) ;
hence |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2 ) - (|.(x1 - x2).| ^2 )) by A1; :: thesis: verum