let n be Element of NAT ; :: thesis: for q being Element of REAL n
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let q be Element of REAL n; :: thesis: for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let p be Point of (TOP-REAL n); :: thesis: for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let i be Element of NAT ; :: thesis: ( i in Seg n & q = p implies ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 ) )
assume that
A1: i in Seg n and
A2: q = p ; :: thesis: ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
reconsider pd = (p /. i) ^2 as Element of REAL by XREAL_0:def 1;
A3: Sum ((0* n) +* (i,pd)) = pd by A1, Th10;
len (0* n) = n by CARD_1:def 7;
then len ((0* n) +* (i,pd)) = n by FUNCT_7:97;
then reconsider w1 = (0* n) +* (i,pd) as Element of n -tuples_on REAL by FINSEQ_2:92;
A4: len w1 = n by CARD_1:def 7;
reconsider w2 = sqr q as Element of n -tuples_on REAL ;
A5: Sum (sqr q) >= 0 by RVSUM_1:86;
A6: len q = n by CARD_1:def 7;
A7: for j being Nat st j in Seg n holds
w1 . j <= w2 . j

proof

let j be Nat; :: thesis: ( j in Seg n implies w1 . j <= w2 . j )
assume A8: j in Seg n ; :: thesis: w1 . j <= w2 . j
set r1 = w1 . j;
set r2 = w2 . j;

per cases ( j = i or j <> i ) ;

suppose A9: j = i ; :: thesis: w1 . j <= w2 . j

then j in dom q by A1, A6, FINSEQ_1:def 3;
then A10: q /. j = q . j by PARTFUN1:def 6;
A11: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
i in dom w1 by A1, A4, FINSEQ_1:def 3;
then w1 . j = w1 /. i by A9, PARTFUN1:def 6
.= (q /. i) ^2 by A2, A1, A11, FUNCT_7:36 ;
hence w1 . j <= w2 . j by A9, A10, VALUED_1:11; :: thesis: verum

end;

suppose A12: j <> i ; :: thesis: w1 . j <= w2 . j

A13: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7 ;
dom q = Seg n by A6, FINSEQ_1:def 3;
then q /. j = q . j by A8, PARTFUN1:def 6;
then A14: w2 . j = (q /. j) ^2 by VALUED_1:11;
j in dom w1 by A4, A8, FINSEQ_1:def 3;
then w1 . j = w1 /. j by PARTFUN1:def 6
.= (0* n) /. j by A8, A12, A13, FUNCT_7:37
.= (n |-> 0) . j by A8, A13, PARTFUN1:def 6
.= 0 by A8, FUNCOP_1:7 ;
hence w1 . j <= w2 . j by A14, XREAL_1:63; :: thesis: verum

end;

end;

end;

then Sum w1 <= Sum w2 by RVSUM_1:82;
then ( 0 <= (p /. i) ^2 & (p /. i) ^2 <= (sqrt (Sum (sqr q))) ^2 ) by A5, A3, SQUARE_1:def 2, XREAL_1:63;
then sqrt ((p /. i) ^2) <= sqrt ((sqrt (Sum (sqr q))) ^2) by SQUARE_1:26;
then |.|.(p /. i).|.| <= sqrt ((sqrt (Sum (sqr q))) ^2) by COMPLEX1:72;
then ( 0 <= |.q.| & |.(p /. i).| <= |.(sqrt (Sum (sqr q))).| ) by COMPLEX1:72;
then A15: |.(p /. i).| <= sqrt (Sum (sqr q)) by ABSVALUE:def 1;
A16: p /. i <= |.(p /. i).| by ABSVALUE:4;
|.q.| ^2 = Sum (sqr q) by A5, SQUARE_1:def 2;
hence ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 ) by A7, A3, A15, A16, RVSUM_1:82, XXREAL_0:2; :: thesis: verum