let n be 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 n = n as Element of NAT by ORDINAL1:def 12;
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 16;
A2: n + 1 = len x by CARD_1:def 7;
then n + 1 in Seg (len x) by FINSEQ_1:4;
then A3: n + 1 in dom x by FINSEQ_1:def 3;
len (x | n) = n by A2, FINSEQ_1:59, NAT_1:11;
then reconsider xn = x | n as Element of n -tuples_on REAL by FINSEQ_2:92;
( sqr x is Element of REAL (n + 1) & ( for k being 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 Nat st k in Seg (n + 1) holds
0 <= (sqr x) . k
let k be 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:63; :: 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 2;
( sqr (x | n) is Element of REAL n & ( for k being 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 Nat st k in Seg n holds
0 <= (sqr (x | n)) . k
let k be 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:63; :: 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 2;
A6: x = x | (n + 1) by A2, FINSEQ_1:58
.= x | (Seg (n + 1)) by FINSEQ_1:def 16
.= (x | n) ^ <*(x . (n + 1))*> by A3, A1, FINSEQ_5:10 ;
(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:74; :: thesis: verum