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 15;

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 ) )

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 ) )

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 15

.= (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

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 15;

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

then
( |.x.| = sqrt (Sum (sqr x)) & 0 <= Sum (sqr x) )
by Th7, EUCLID:def 5;
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;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

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

then
( |.(x | n).| = sqrt (Sum (sqr (x | n))) & 0 <= Sum (sqr (x | n)) )
by Th7, EUCLID:def 5;
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;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

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 15

.= (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