let n be Nat; :: thesis: for x1, x2 being Element of REAL n holds |.(x1 + x2).| <= |.x1.| + |.x2.|
let x1, x2 be Element of REAL n; :: thesis: |.(x1 + x2).| <= |.x1.| + |.x2.|
A1: 0 <= Sum (sqr (x1 + x2)) by RVSUM_1:86;
A2: 0 <= Sum (sqr (abs x1)) by RVSUM_1:86;
then A3: 0 <= sqrt (Sum (sqr (abs x1))) by SQUARE_1:def 2;
A4: for k being Nat st k in Seg n holds
(sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k

proof

let k be Nat; :: thesis: ( k in Seg n implies (sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k )
len (x1 + x2) = n by CARD_1:def 7;
then A5: dom (x1 + x2) = Seg n by FINSEQ_1:def 3;
assume A6: k in Seg n ; :: thesis: (sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k
reconsider abs1 = (abs x1) . k, abs2 = (abs x2) . k as Real ;
reconsider r12 = (x1 + x2) . k as Element of REAL by XREAL_0:def 1;
reconsider r11 = x1 . k, r22 = x2 . k as Element of REAL by XREAL_0:def 1;
|.(r11 + r22).| <= |.r11.| + |.r22.| by COMPLEX1:56;
then |.r12.| <= |.r11.| + |.r22.| by A6, A5, VALUED_1:def 1;
then |.r12.| <= |.r11.| + abs2 by VALUED_1:18;
then A7: |.r12.| <= abs1 + abs2 by VALUED_1:18;
reconsider abs912 = (abs (x1 + x2)) . k as Real ;
reconsider abs12 = ((abs x1) + (abs x2)) . k as Real ;
set r2 = (sqr ((abs x1) + (abs x2))) . k;
|.r12.| >= 0 by COMPLEX1:46;
then A8: 0 <= abs912 by VALUED_1:18;
len ((abs x1) + (abs x2)) = n by CARD_1:def 7;
then dom ((abs x1) + (abs x2)) = Seg n by FINSEQ_1:def 3;
then |.r12.| <= abs12 by A6, A7, VALUED_1:def 1;
then abs912 <= abs12 by VALUED_1:18;
then abs912 ^2 <= abs12 ^2 by A8, SQUARE_1:15;
then abs912 ^2 <= (sqr ((abs x1) + (abs x2))) . k by VALUED_1:11;
hence (sqr (abs (x1 + x2))) . k <= (sqr ((abs x1) + (abs x2))) . k by VALUED_1:11; :: thesis: verum

end;

0 <= (Sum (mlt ((abs x1),(abs x2)))) ^2 by XREAL_1:63;
then A9: sqrt ((Sum (mlt ((abs x1),(abs x2)))) ^2) <= sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2)))) by RVSUM_1:92, SQUARE_1:26;
A10: for k being Nat st k in Seg n holds
0 <= (mlt ((abs x1),(abs x2))) . k

proof

let k be Nat; :: thesis: ( k in Seg n implies 0 <= (mlt ((abs x1),(abs x2))) . k )
assume k in Seg n ; :: thesis: 0 <= (mlt ((abs x1),(abs x2))) . k
set r = (mlt ((abs x1),(abs x2))) . k;
reconsider r1 = x1 . k, r2 = x2 . k as Element of REAL by XREAL_0:def 1;
( (abs x1) . k = |.r1.| & (abs x2) . k = |.r2.| ) by VALUED_1:18;
then A11: (mlt ((abs x1),(abs x2))) . k = |.r1.| * |.r2.| by RVSUM_1:60;
( 0 <= |.r1.| & 0 <= |.r2.| ) by COMPLEX1:46;
hence 0 <= (mlt ((abs x1),(abs x2))) . k by A11; :: thesis: verum

end;

len (mlt ((abs x1),(abs x2))) = n by CARD_1:def 7;
then dom (mlt ((abs x1),(abs x2))) = Seg n by FINSEQ_1:def 3;
then Sum (mlt ((abs x1),(abs x2))) <= sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2)))) by A10, A9, RVSUM_1:84, SQUARE_1:22;
then 2 * (Sum (mlt ((abs x1),(abs x2)))) <= 2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2))))) by XREAL_1:64;
then (Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2))))) <= (Sum (sqr (abs x1))) + (2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2)))))) by XREAL_1:7;
then A12: ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) <= ((Sum (sqr (abs x1))) + (2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2))))))) + (Sum (sqr (abs x2))) by XREAL_1:7;
A13: 0 <= Sum (sqr (abs x2)) by RVSUM_1:86;
then A14: 0 <= sqrt (Sum (sqr (abs x2))) by SQUARE_1:def 2;
Sum (sqr ((abs x1) + (abs x2))) = Sum (((sqr (abs x1)) + (2 * (mlt ((abs x1),(abs x2))))) + (sqr (abs x2))) by RVSUM_1:68
.= (Sum ((sqr (abs x1)) + (2 * (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by RVSUM_1:89
.= ((Sum (sqr (abs x1))) + (Sum (2 * (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by RVSUM_1:89
.= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by RVSUM_1:87 ;
then Sum (sqr (abs (x1 + x2))) <= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by A4, RVSUM_1:82;
then Sum (sqr (x1 + x2)) <= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt ((abs x1),(abs x2)))))) + (Sum (sqr (abs x2))) by Lm2;
then Sum (sqr (x1 + x2)) <= ((Sum (sqr (abs x1))) + (2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2))))))) + (Sum (sqr (abs x2))) by A12, XXREAL_0:2;
then A15: Sum (sqr (x1 + x2)) <= ((Sum (sqr (abs x1))) + (2 * ((sqrt (Sum (sqr (abs x1)))) * (sqrt (Sum (sqr (abs x2))))))) + (Sum (sqr (abs x2))) by A2, A13, SQUARE_1:29;
A16: (sqrt (Sum (sqr (abs x2)))) ^2 = Sum (sqr (abs x2)) by A13, SQUARE_1:def 2;
Sum (sqr (abs x1)) = (sqrt (Sum (sqr (abs x1)))) ^2 by A2, SQUARE_1:def 2;
then sqrt (Sum (sqr (x1 + x2))) <= sqrt (((sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr (abs x2))))) ^2) by A15, A16, A1, SQUARE_1:26;
then sqrt (Sum (sqr (x1 + x2))) <= (sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr (abs x2)))) by A3, A14, SQUARE_1:22;
then sqrt (Sum (sqr (x1 + x2))) <= (sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr x2))) by Lm2;
hence |.(x1 + x2).| <= |.x1.| + |.x2.| by Lm2; :: thesis: verum