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
( Proj p,i <= |.q.| & (Proj 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
( Proj p,i <= |.q.| & (Proj 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
( Proj p,i <= |.q.| & (Proj p,i) ^2 <= |.q.| ^2 )
let i be Element of NAT ; :: thesis: ( i in Seg n & q = p implies ( Proj p,i <= |.q.| & (Proj p,i) ^2 <= |.q.| ^2 ) )
assume A1: ( i in Seg n & q = p ) ; :: thesis: ( Proj p,i <= |.q.| & (Proj p,i) ^2 <= |.q.| ^2 )
A2: Sum (sqr q) >= 0 by RVSUM_1:116;
then A3: |.q.| ^2 = Sum (sqr q) by SQUARE_1:def 4;
A4: 0 <= |.q.| ;
A5: len q = n by FINSEQ_1:def 18;
len (0* n) = n by FINSEQ_1:def 18;
then len ((0* n) +* i,((Proj p,i) ^2 )) = n by FUNCT_7:99;
then reconsider w1 = (0* n) +* i,((Proj p,i) ^2 ) as Element of n -tuples_on REAL by FINSEQ_2:110;
A6: len w1 = n by FINSEQ_1:def 18;
reconsider w2 = sqr q as Element of n -tuples_on REAL ;
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

A10: i in dom w1 by A1, A6, FINSEQ_1:def 3;
A11: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
A12: w1 . j = w1 /. i by A9, A10, PARTFUN1:def 8
.= (Proj p,i) ^2 by A1, A11, FUNCT_7:38
.= (q /. i) ^2 by A1, Def1 ;
j in dom q by A1, A5, A9, FINSEQ_1:def 3;
then q /. j = q . j by PARTFUN1:def 8;
hence w1 . j <= w2 . j by A9, A12, VALUED_1:11; :: thesis: verum

end;

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

A14: j in dom w1 by A6, A8, FINSEQ_1:def 3;
A15: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def 3
.= Seg n by FINSEQ_1:def 18 ;
A16: w1 . j = w1 /. j by A14, PARTFUN1:def 8
.= (0* n) /. j by A8, A13, A15, FUNCT_7:39
.= (n |-> 0 ) . j by A8, A15, PARTFUN1:def 8
.= 0 by A8, FUNCOP_1:13 ;
dom q = Seg n by A5, FINSEQ_1:def 3;
then q /. j = q . j by A8, PARTFUN1:def 8;
then w2 . j = (q /. j) ^2 by VALUED_1:11;
hence w1 . j <= w2 . j by A16, XREAL_1:65; :: thesis: verum

end;

end;

end;

then A17: Sum w1 <= Sum w2 by RVSUM_1:112;
A18: Sum ((0* n) +* i,((Proj p,i) ^2 )) = (Proj p,i) ^2 by A1, Th14;
A19: 0 <= (Proj p,i) ^2 by XREAL_1:65;
(Proj p,i) ^2 <= (sqrt (Sum (sqr q))) ^2 by A2, A17, A18, SQUARE_1:def 4;
then sqrt ((Proj p,i) ^2 ) <= sqrt ((sqrt (Sum (sqr q))) ^2 ) by A19, SQUARE_1:94;
then abs (abs (Proj p,i)) <= sqrt ((sqrt (Sum (sqr q))) ^2 ) by COMPLEX1:158;
then abs (Proj p,i) <= abs (sqrt (Sum (sqr q))) by COMPLEX1:158;
then A20: abs (Proj p,i) <= sqrt (Sum (sqr q)) by A4, ABSVALUE:def 1;
Proj p,i <= abs (Proj p,i) by ABSVALUE:11;
hence ( Proj p,i <= |.q.| & (Proj p,i) ^2 <= |.q.| ^2 ) by A3, A7, A18, A20, RVSUM_1:112, XXREAL_0:2; :: thesis: verum