let n be Nat; :: thesis: for x being Element of REAL n
for xMAX being Real st xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) holds
( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
let x be Element of REAL n; :: thesis: for xMAX being Real st xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) holds
( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
let xMAX be Real; :: thesis: ( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) implies ( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) ) )
assume A1: ( xMAX in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= xMAX ) ) ; :: thesis: ( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) )
len x = n by CARD_1:def 7;
then A2: dom x = Seg n by FINSEQ_1:def 3;
A3: dom (abs x) = dom x by VALUED_1:def 11;
set F = n |-> xMAX;
for j being Nat st j in Seg n holds
(abs x) . j <= (n |-> xMAX) . j

proof

let j be Nat; :: thesis: ( j in Seg n implies (abs x) . j <= (n |-> xMAX) . j )
assume A4: j in Seg n ; :: thesis: (abs x) . j <= (n |-> xMAX) . j
then (abs x) . j <= xMAX by A1, A2;
hence (abs x) . j <= (n |-> xMAX) . j by A4, FINSEQ_2:57; :: thesis: verum

end;

then A5: Sum (abs x) <= Sum (n |-> xMAX) by RVSUM_1:82;
consider i being object such that
A6: ( i in dom (abs x) & xMAX = (abs x) . i ) by A1, FUNCT_1:def 3;
reconsider i = i as Element of NAT by A6;
A7: (abs x) . i = absreal . (x . i) by A3, A6, FUNCT_1:13
.= |.(x . i).| by EUCLID:def 2 ;
reconsider y = x as Point of (TOP-REAL n) by EUCLID:22;
reconsider y = y as FinSequence of REAL ;
defpred S₁[ Nat] means for x being Element of REAL $1 holds |.x.| ^2 <= (Sum (abs x)) ^2 ;
A8: S₁[ 0 ] by RVSUM_1:72;
A9: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A10: S₁[n] ; :: thesis: S₁[n + 1]
let x be Element of REAL (n + 1); :: thesis: |.x.| ^2 <= (Sum (abs x)) ^2
set y = x | n;
A11: len x = n + 1 by CARD_1:def 7;
A12: x | n is Element of (len (x | n)) -tuples_on REAL by FINSEQ_2:92;
reconsider y = x | n as Element of REAL n by A11, A12, NAT_1:11, FINSEQ_1:59;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom x by A11, FINSEQ_1:def 3;
then x . (n + 1) in rng x by FUNCT_1:3;
then reconsider w = x . (n + 1) as Element of REAL ;
A13: x = y ^ <*w*> by A11, FINSEQ_3:55;
A14: 0 <= Sum (sqr y) by RVSUM_1:86;
A15: 0 <= Sum (sqr x) by RVSUM_1:86;
sqr x = (sqr y) ^ <*(sqrreal . w)*> by A13, FINSEQOP:8;
then A16: Sum (sqr x) = (Sum (sqr y)) + (sqrreal . w) by RVSUM_1:74
.= (Sum (sqr y)) + (w ^2) by RVSUM_1:def 2
.= (|.y.| ^2) + (w ^2) by A14, SQUARE_1:def 2 ;
A17: |.x.| ^2 = Sum (sqr x) by A15, SQUARE_1:def 2;
abs x = (abs y) ^ (abs <*w*>) by A13, FINSEQOP:9
.= (abs y) ^ <*|.w.|*> by JORDAN2B:19 ;
then (Sum (abs x)) ^2 = ((Sum (abs y)) + |.w.|) ^2 by RVSUM_1:74
.= (((Sum (abs y)) ^2) + ((2 * (Sum (abs y))) * |.w.|)) + (|.w.| ^2)
.= (((Sum (abs y)) ^2) + ((2 * (Sum (abs y))) * |.w.|)) + (w ^2) by COMPLEX1:75 ;
then A18: ((Sum (abs x)) ^2) - (|.x.| ^2) = (((Sum (abs y)) ^2) - (|.y.| ^2)) + ((2 * (Sum (abs y))) * |.w.|) by A16, A17;
A19: 0 <= ((Sum (abs y)) ^2) - (|.y.| ^2) by A10, XREAL_1:48;
( 0 <= |.w.| & 0 <= Sum (abs y) ) by Th9;
hence |.x.| ^2 <= (Sum (abs x)) ^2 by A18, A19, XREAL_1:49; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A9);
then A20: |.x.| ^2 <= (Sum (abs x)) ^2 ;
n is Element of NAT by ORDINAL1:def 12;
then |.(y /. i).| <= |.x.| by A2, A3, A6, PDIFF_8:1;
hence ( Sum (abs x) <= n * xMAX & xMAX <= |.x.| & |.x.| <= Sum (abs x) ) by A3, A5, A6, A7, A20, Th9, PARTFUN1:def 6, RVSUM_1:80, SQUARE_1:16; :: thesis: verum