let n be Nat; :: thesis: for x being Element of REAL (n + 1)
for y being Element of REAL n
for w being Element of REAL st y = x | n & w = x . (n + 1) holds
|.x.| <= |.y.| + |.w.|
let x be Element of REAL (n + 1); :: thesis: for y being Element of REAL n
for w being Element of REAL st y = x | n & w = x . (n + 1) holds
|.x.| <= |.y.| + |.w.|
let y be Element of REAL n; :: thesis: for w being Element of REAL st y = x | n & w = x . (n + 1) holds
|.x.| <= |.y.| + |.w.|
let w be Element of REAL ; :: thesis: ( y = x | n & w = x . (n + 1) implies |.x.| <= |.y.| + |.w.| )
assume A1: ( y = x | n & w = x . (n + 1) ) ; :: thesis: |.x.| <= |.y.| + |.w.|
len x = n + 1 by CARD_1:def 7;
then x = y ^ <*w*> by A1, FINSEQ_3:55;
then sqr x = (sqr y) ^ <*(sqrreal . w)*> by FINSEQOP:8;
then A3: Sum (sqr x) = (Sum (sqr y)) + (sqrreal . w) by RVSUM_1:74;
A4: 0 <= Sum (sqr y) by RVSUM_1:86;
A5: sqrreal . w = w ^2 by RVSUM_1:def 2;
then 0 <= sqrreal . w by XREAL_1:63;
then sqrt (Sum (sqr x)) <= (sqrt (Sum (sqr y))) + (sqrt (sqrreal . w)) by A3, A4, SQUARE_1:59;
hence |.x.| <= |.y.| + |.w.| by A5, COMPLEX1:72; :: thesis: verum