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;

|.(x . i).| * |.(x . i).| = (x . i) ^2

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

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

A2:
0 <= |.(x . i).| * |.(x . i).|
by XREAL_1:63;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;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

|.(x . i).| * |.(x . i).| = (x . i) ^2

proof
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