let n, i be Element of NAT ; :: thesis: for q being Element of REAL n
for p being Point of (TOP-REAL n) st i in Seg n & q = p holds
|.(p /. i).| <= |.q.|
let q be Element of REAL n; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n & q = p holds
|.(p /. i).| <= |.q.|
let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n & q = p implies |.(p /. i).| <= |.q.| )
assume that
A1: i in Seg n and
A2: q = p ; :: thesis: |.(p /. i).| <= |.q.|
reconsider p2 = (p /. i) ^2 , q2 = (q /. i) ^2 as Element of REAL by XREAL_0:def 1;
A3: Sum ((0* n) +* (i,p2)) = (p /. i) ^2 by A1, JORDAN2B:10;
len (0* n) = n by CARD_1:def 7;
then len ((0* n) +* (i,p2)) = n by FUNCT_7:97;
then reconsider w1 = (0* n) +* (i,p2) 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;
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 A7: 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 A8: j = i ; :: thesis: w1 . j <= w2 . j

then j in dom q by A1, A6, FINSEQ_1:def 3;
then A9: q /. j = q . j by PARTFUN1:def 6;
A10: 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 A8, PARTFUN1:def 6
.= q2 by A2, A1, A10, FUNCT_7:36 ;
hence w1 . j <= w2 . j by A8, A9, VALUED_1:11; :: thesis: verum

end;

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

A12: 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 A7, PARTFUN1:def 6;
then A13: w2 . j = (q /. j) ^2 by VALUED_1:11;
j in dom w1 by A4, A7, FINSEQ_1:def 3;
then w1 . j = w1 /. j by PARTFUN1:def 6
.= (0* n) /. j by A7, A11, A12, FUNCT_7:37
.= (n |-> 0) . j by A7, A12, PARTFUN1:def 6
.= 0 ;
hence w1 . j <= w2 . j by A13, 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;
hence |.(p /. i).| <= |.q.| by ABSVALUE:def 1; :: thesis: verum