let n be Nat; :: thesis: for y1, y2 being real-valued FinSequence
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 real-valued FinSequence; :: 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))
reconsider w1 = x1, w2 = x2 as Element of n -tuples_on REAL by EUCLID:def 1;
set v1 = sqr (x1 + x2);
set v2 = sqr (x1 - x2);
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:86;
then A3: (sqrt (Sum (sqr (x1 + x2)))) ^2 = Sum (sqr (x1 + x2)) by SQUARE_1:def 2;
A4: (Sum (sqr (x1 + x2))) - (Sum (sqr (x1 - x2))) = Sum ((sqr (x1 + x2)) - (sqr (x1 - x2))) by RVSUM_1:90;
Sum (sqr (x1 - x2)) >= 0 by RVSUM_1:86;
then A5: (sqrt (Sum (sqr (x1 - x2)))) ^2 = Sum (sqr (x1 - x2)) by SQUARE_1:def 2;
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:28 ;
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:68
.= (((sqr w1) + (2 * (mlt (w1,w2)))) + (sqr w2)) - (((sqr w1) - (2 * (mlt (w1,w2)))) + (sqr w2)) by RVSUM_1:69
.= (((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - (((sqr w1) - (2 * (mlt (w1,w2)))) + (sqr w2)) by A7, FINSEQOP:28
.= ((((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - ((sqr w1) - (2 * (mlt (w1,w2))))) - (sqr w2) by RVSUM_1:39
.= (((((2 * (mlt (w1,w2))) + (sqr w2)) + (sqr w1)) - (sqr w1)) + (2 * (mlt (w1,w2)))) - (sqr w2) by RVSUM_1:41
.= (((2 * (mlt (w1,w2))) + (sqr w2)) + (2 * (mlt (w1,w2)))) - (sqr w2) by RVSUM_1:42
.= (2 * (mlt (w1,w2))) + (2 * (mlt (w1,w2))) by A6, RVSUM_1:42
.= (2 + 2) * (mlt (w1,w2)) by RVSUM_1:50
.= 4 * (mlt (w1,w2)) ;
then (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) = (1 / 4) * (4 * (Sum (mlt (w1,w2)))) by A2, A3, A5, A4, RVSUM_1:87
.= Sum (mlt (w1,w2)) ;
hence |(y1,y2)| = (1 / 4) * ((|.(x1 + x2).| ^2) - (|.(x1 - x2).| ^2)) by A1; :: thesis: verum