let n be Nat; :: thesis: for x being Element of REAL n
for i being Nat st i in Seg n holds
|.(x . i).| <= |.x.|
let x be Element of REAL n; :: thesis: for i being Nat st i in Seg n holds
|.(x . i).| <= |.x.|
let i be Nat; :: thesis: ( i in Seg n implies |.(x . i).| <= |.x.| )
reconsider sx = sqr x as Element of REAL n by EUCLID:def 1;

A1: now :: thesis: for k being Nat st k in Seg n holds
0 <= sx . k

let k be Nat; :: thesis: ( k in Seg n implies 0 <= sx . k )
assume k in Seg n ; :: thesis: 0 <= sx . k
sx . k = (x . k) ^2 by VALUED_1:11;
hence 0 <= sx . k by XREAL_1:63; :: thesis: verum

end;

A2: 0 <= |.(x . i).| * |.(x . i).| by XREAL_1:63;
|.(x . i).| * |.(x . i).| = (x . i) ^2

proof

per cases ( |.(x . i).| = x . i or |.(x . i).| = - (x . i) ) by ABSVALUE:1;

suppose |.(x . i).| = x . i ; :: thesis: |.(x . i).| * |.(x . i).| = (x . i) ^2

hence |.(x . i).| * |.(x . i).| = (x . i) ^2 ; :: thesis: verum

end;

suppose |.(x . i).| = - (x . i) ; :: thesis: |.(x . i).| * |.(x . i).| = (x . i) ^2

hence |.(x . i).| * |.(x . i).| = (x . i) ^2 ; :: thesis: verum

end;

end;

end;

then A3: (sqr x) . i = |.(x . i).| * |.(x . i).| by VALUED_1:11;
assume i in Seg n ; :: thesis: |.(x . i).| <= |.x.|
then |.(x . i).| * |.(x . i).| <= Sum (sqr x) by A3, A1, Th7;
then A4: sqrt (|.(x . i).| * |.(x . i).|) <= sqrt (Sum (sqr x)) by A2, SQUARE_1:26;
sqrt (|.(x . i).| ^2) = |.(x . i).| by COMPLEX1:46, SQUARE_1:22;
hence |.(x . i).| <= |.x.| by A4, EUCLID:def 5; :: thesis: verum