let n be Element of NAT ; :: thesis: for x being Element of REAL (n + 1) holds |.x.| ^2 = (|.(x | n).| ^2 ) + ((x . (n + 1)) ^2 )
let x be Element of REAL (n + 1); :: thesis: |.x.| ^2 = (|.(x | n).| ^2 ) + ((x . (n + 1)) ^2 )
reconsider x = x as Element of (n + 1) -tuples_on REAL by EUCLID:def 1;
A1: x | n = x | (Seg n) by FINSEQ_1:def 15;
A2: n + 1 = len x by FINSEQ_1:def 18;
then n + 1 in Seg (len x) by FINSEQ_1:6;
then A3: n + 1 in dom x by FINSEQ_1:def 3;
len (x | n) = n by A2, FINSEQ_1:80, NAT_1:11;
then reconsider xn = x | n as Element of n -tuples_on REAL by FINSEQ_2:110;
( sqr x is Element of REAL (n + 1) & ( for k being Element of NAT st k in Seg (n + 1) holds
0 <= (sqr x) . k ) )

proof

thus sqr x is Element of REAL (n + 1) by EUCLID:def 1; :: thesis: for k being Element of NAT st k in Seg (n + 1) holds
0 <= (sqr x) . k
let k be Element of NAT ; :: thesis: ( k in Seg (n + 1) implies 0 <= (sqr x) . k )
assume k in Seg (n + 1) ; :: thesis: 0 <= (sqr x) . k
(sqr x) . k = (x . k) ^2 by VALUED_1:11
.= (x . k) * (x . k) ;
hence 0 <= (sqr x) . k by XREAL_1:65; :: thesis: verum

end;

then ( |.x.| = sqrt (Sum (sqr x)) & 0 <= Sum (sqr x) ) by Th7, EUCLID:def 5;
then A4: |.x.| ^2 = Sum (sqr x) by SQUARE_1:def 4;
( sqr (x | n) is Element of REAL n & ( for k being Element of NAT st k in Seg n holds
0 <= (sqr (x | n)) . k ) )

proof

sqr xn is Element of REAL n by EUCLID:def 1;
hence sqr (x | n) is Element of REAL n ; :: thesis: for k being Element of NAT st k in Seg n holds
0 <= (sqr (x | n)) . k
let k be Element of NAT ; :: thesis: ( k in Seg n implies 0 <= (sqr (x | n)) . k )
assume k in Seg n ; :: thesis: 0 <= (sqr (x | n)) . k
(sqr xn) . k = (xn . k) ^2 by VALUED_1:11
.= (xn . k) * (xn . k) ;
hence 0 <= (sqr (x | n)) . k by XREAL_1:65; :: thesis: verum

end;

then ( |.(x | n).| = sqrt (Sum (sqr (x | n))) & 0 <= Sum (sqr (x | n)) ) by Th7, EUCLID:def 5;
then A5: (|.(x | n).| ^2 ) + ((x . (n + 1)) ^2 ) = (Sum (sqr (x | n))) + ((x . (n + 1)) ^2 ) by SQUARE_1:def 4;
A6: x = x | (n + 1) by A2, FINSEQ_1:79
.= x | (Seg (n + 1)) by FINSEQ_1:def 15
.= (x | n) ^ <*(x . (n + 1))*> by A3, A1, FINSEQ_5:11 ;
(sqr (x | n)) ^ <*((x . (n + 1)) ^2 )*> = (mlt xn,xn) ^ <*((x . (n + 1)) * (x . (n + 1)))*>
.= mlt (xn ^ <*(x . (n + 1))*>),((x | n) ^ <*(x . (n + 1))*>) by RFUNCT_4:2
.= sqr x by A6 ;
hence |.x.| ^2 = (|.(x | n).| ^2 ) + ((x . (n + 1)) ^2 ) by A4, A5, RVSUM_1:104; :: thesis: verum