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:116;
A2: 0 <= Sum (sqr (abs x1)) by RVSUM_1:116;
then A3: 0 <= sqrt (Sum (sqr (abs x1))) by SQUARE_1:def 4;
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 FINSEQ_1:def 18;
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 ;
reconsider r11 = x1 . k, r22 = x2 . k as Element of REAL ;
abs (r11 + r22) <= (abs r11) + (abs r22) by COMPLEX1:142;
then abs r12 <= (abs r11) + (abs r22) by A6, A5, VALUED_1:def 1;
then abs r12 <= (abs r11) + abs2 by VALUED_1:18;
then A7: abs 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;
abs r12 >= 0 by COMPLEX1:132;
then A8: 0 <= abs912 by VALUED_1:18;
len ((abs x1) + (abs x2)) = n by FINSEQ_1:def 18;
then dom ((abs x1) + (abs x2)) = Seg n by FINSEQ_1:def 3;
then abs 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:77;
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:65;
then A9: sqrt ((Sum (mlt (abs x1),(abs x2))) ^2 ) <= sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2)))) by RVSUM_1:122, SQUARE_1:94;
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 ;
( (abs x1) . k = abs r1 & (abs x2) . k = abs r2 ) by VALUED_1:18;
then A11: (mlt (abs x1),(abs x2)) . k = (abs r1) * (abs r2) by RVSUM_1:87;
( 0 <= abs r1 & 0 <= abs r2 ) by COMPLEX1:132;
hence 0 <= (mlt (abs x1),(abs x2)) . k by A11; :: thesis: verum

end;

len (mlt (abs x1),(abs x2)) = n by FINSEQ_1:def 18;
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:114, SQUARE_1:89;
then 2 * (Sum (mlt (abs x1),(abs x2))) <= 2 * (sqrt ((Sum (sqr (abs x1))) * (Sum (sqr (abs x2))))) by XREAL_1:66;
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:9;
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:9;
A13: 0 <= Sum (sqr (abs x2)) by RVSUM_1:116;
then A14: 0 <= sqrt (Sum (sqr (abs x2))) by SQUARE_1:def 4;
Sum (sqr ((abs x1) + (abs x2))) = Sum (((sqr (abs x1)) + (2 * (mlt (abs x1),(abs x2)))) + (sqr (abs x2))) by RVSUM_1:98
.= (Sum ((sqr (abs x1)) + (2 * (mlt (abs x1),(abs x2))))) + (Sum (sqr (abs x2))) by RVSUM_1:119
.= ((Sum (sqr (abs x1))) + (Sum (2 * (mlt (abs x1),(abs x2))))) + (Sum (sqr (abs x2))) by RVSUM_1:119
.= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt (abs x1),(abs x2))))) + (Sum (sqr (abs x2))) by RVSUM_1:117 ;
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:112;
then Sum (sqr (x1 + x2)) <= ((Sum (sqr (abs x1))) + (2 * (Sum (mlt (abs x1),(abs x2))))) + (Sum (sqr (abs x2))) by Lm3;
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:97;
A16: (sqrt (Sum (sqr (abs x2)))) ^2 = Sum (sqr (abs x2)) by A13, SQUARE_1:def 4;
Sum (sqr (abs x1)) = (sqrt (Sum (sqr (abs x1)))) ^2 by A2, SQUARE_1:def 4;
then sqrt (Sum (sqr (x1 + x2))) <= sqrt (((sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr (abs x2))))) ^2 ) by A15, A16, A1, SQUARE_1:94;
then sqrt (Sum (sqr (x1 + x2))) <= (sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr (abs x2)))) by A3, A14, SQUARE_1:89;
then sqrt (Sum (sqr (x1 + x2))) <= (sqrt (Sum (sqr (abs x1)))) + (sqrt (Sum (sqr x2))) by Lm3;
hence |.(x1 + x2).| <= |.x1.| + |.x2.| by Lm3; :: thesis: verum