let n be Nat; :: thesis: for x being Element of REAL (n + 1)
for y being Element of REAL n st y = x | n holds
|.y.| <= |.x.|
let x be Element of REAL (n + 1); :: thesis: for y being Element of REAL n st y = x | n holds
|.y.| <= |.x.|
let y be Element of REAL n; :: thesis: ( y = x | n implies |.y.| <= |.x.| )
assume A1: y = x | n ; :: thesis: |.y.| <= |.x.|
A2: len x = n + 1 by CARD_1:def 7;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom x by A2, FINSEQ_1:def 3;
then x . (n + 1) in rng x by FUNCT_1:3;
then reconsider xn = x . (n + 1) as Element of REAL ;
x = y ^ <*xn*> by A1, A2, FINSEQ_3:55;
then sqr x = (sqr y) ^ <*(sqrreal . xn)*> by FINSEQOP:8;
then A4: Sum (sqr x) = (Sum (sqr y)) + (sqrreal . xn) by RVSUM_1:74;
A5: 0 <= Sum (sqr y) by RVSUM_1:86;
sqrreal . xn = xn ^2 by RVSUM_1:def 2;
then 0 <= sqrreal . xn by XREAL_1:63;
then 0 + (Sum (sqr y)) <= Sum (sqr x) by A4, XREAL_1:7;
hence |.y.| <= |.x.| by A5, SQUARE_1:26; :: thesis: verum