let n be Element of NAT ; :: thesis: for x being Element of REAL n
for i being Element of NAT st i in Seg n holds
abs (x . i) <= |.x.|
let x be Element of REAL n; :: thesis: for i being Element of NAT st i in Seg n holds
abs (x . i) <= |.x.|
let i be Element of NAT ; :: thesis: ( i in Seg n implies abs (x . i) <= |.x.| )
assume A1: i in Seg n ; :: thesis: abs (x . i) <= |.x.|
(abs (x . i)) * (abs (x . i)) = (x . i) ^2

proof

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

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

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

end;

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

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

end;

end;

end;

then A2: (sqr x) . i = (abs (x . i)) * (abs (x . i)) by VALUED_1:11;
reconsider sx = sqr x as Element of REAL n by EUCLID:def 1;

now

let k be Element of 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:65; :: thesis: verum

end;

then A3: (abs (x . i)) * (abs (x . i)) <= Sum (sqr x) by A1, A2, Th7;
0 <= (abs (x . i)) * (abs (x . i)) by XREAL_1:65;
then A4: sqrt ((abs (x . i)) * (abs (x . i))) <= sqrt (Sum (sqr x)) by A3, SQUARE_1:94;
sqrt ((abs (x . i)) ^2 ) = abs (x . i) by COMPLEX1:132, SQUARE_1:89;
hence abs (x . i) <= |.x.| by A4, EUCLID:def 5; :: thesis: verum