let n be non empty Nat; :: thesis: for x, y being Element of REAL n
for a being Real holds
( 0 <= (max_norm n) . x & ( (max_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (max_norm n) . x = 0 ) & (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) & (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) )
let x, y be Element of REAL n; :: thesis: for a being Real holds
( 0 <= (max_norm n) . x & ( (max_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (max_norm n) . x = 0 ) & (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) & (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) )
let a be Real; :: thesis: ( 0 <= (max_norm n) . x & ( (max_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (max_norm n) . x = 0 ) & (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) & (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) )
set xMAX = (max_norm n) . x;
set yMAX = (max_norm n) . y;
set axMAX = (max_norm n) . (a * x);
set xyMAX = (max_norm n) . (x + y);
A1: ( (max_norm n) . x in rng (abs x) & ( for i being Nat st i in dom x holds
(abs x) . i <= (max_norm n) . x ) ) by Def1;
A2: ( (max_norm n) . (a * x) in rng (abs (a * x)) & ( for i being Nat st i in dom (a * x) holds
(abs (a * x)) . i <= (max_norm n) . (a * x) ) ) by Def1;
A3: ( (max_norm n) . (x + y) in rng (abs (x + y)) & ( for i being Nat st i in dom (x + y) holds
(abs (x + y)) . i <= (max_norm n) . (x + y) ) ) by Def1;
A4: dom x = dom (abs x) by VALUED_1:def 11;
A5: dom y = dom (abs y) by VALUED_1:def 11;
A6: len x = n by CARD_1:def 7;
then A7: dom x = Seg n by FINSEQ_1:def 3;
len y = n by CARD_1:def 7;
then A8: dom y = Seg n by FINSEQ_1:def 3;
len (x + y) = n by CARD_1:def 7;
then A9: dom (x + y) = Seg n by FINSEQ_1:def 3;
(max_norm n) . x in rng (abs x) by Def1;
then consider j0 being object such that
A10: ( j0 in dom (abs x) & (max_norm n) . x = (abs x) . j0 ) by FUNCT_1:def 3;
reconsider j0 = j0 as Nat by A10;
(abs x) . j0 = |.(x . j0).| by A10, VALUED_1:def 11;
hence 0 <= (max_norm n) . x by A10; :: thesis: ( ( (max_norm n) . x = 0 implies x = 0* n ) & ( x = 0* n implies (max_norm n) . x = 0 ) & (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) & (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) )
(max_norm n) . y in rng (abs y) by Def1;
then consider k0 being object such that
A11: ( k0 in dom (abs y) & (max_norm n) . y = (abs y) . k0 ) by FUNCT_1:def 3;
reconsider k0 = k0 as Nat by A11;
thus ( (max_norm n) . x = 0 iff x = 0* n ) :: thesis: ( (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) & (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) )

proof

hereby :: thesis: ( x = 0* n implies (max_norm n) . x = 0 )

assume A12: (max_norm n) . x = 0 ; :: thesis: x = 0* n
for i being object st i in dom x holds
x . i = 0

proof

let i0 be object ; :: thesis: ( i0 in dom x implies x . i0 = 0 )
assume A13: i0 in dom x ; :: thesis: x . i0 = 0
then reconsider i = i0 as Nat ;
(abs x) . i <= 0 by A12, A13, Def1;
then |.(x . i).| <= 0 by A4, A13, VALUED_1:def 11;
hence x . i0 = 0 ; :: thesis: verum

end;

hence x = (dom x) --> 0 by FUNCOP_1:11
.= (Seg n) --> (In (0,REAL)) by A6, FINSEQ_1:def 3
.= 0* n by FINSEQ_2:def 2 ;
:: thesis: verum

end;

assume A14: x = 0* n ; :: thesis: (max_norm n) . x = 0
consider j being object such that
A15: ( j in dom (abs x) & (max_norm n) . x = (abs x) . j ) by A1, FUNCT_1:def 3;
reconsider j = j as Nat by A15;
(abs x) . j = |.(x . j).| by A15, VALUED_1:def 11
.= 0 by A14 ;
hence (max_norm n) . x = 0 by A15; :: thesis: verum

end;

thus (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) :: thesis: (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y)

proof

set L = |.a.| * ((max_norm n) . x);
A16: dom (abs (a * x)) = dom (a * x) by VALUED_1:def 11;
A17: dom (a * x) = dom x by VALUED_1:def 5;
A18: j0 in dom (a * x) by A4, A10, VALUED_1:def 5;
then (abs (a * x)) . j0 = |.((a * x) . j0).| by A16, VALUED_1:def 11
.= |.(a * (x . j0)).| by A18, VALUED_1:def 5
.= |.a.| * |.(x . j0).| by COMPLEX1:65
.= |.a.| * ((max_norm n) . x) by A10, VALUED_1:def 11 ;
then A19: |.a.| * ((max_norm n) . x) <= (max_norm n) . (a * x) by Def1, A18;
consider k0 being object such that
A20: ( k0 in dom (abs (a * x)) & (max_norm n) . (a * x) = (abs (a * x)) . k0 ) by FUNCT_1:def 3, A2;
reconsider j0 = j0 as Nat ;
A21: (abs (a * x)) . k0 = |.((a * x) . k0).| by A20, VALUED_1:def 11
.= |.(a * (x . k0)).| by A16, A20, VALUED_1:def 5
.= |.a.| * |.(x . k0).| by COMPLEX1:65 ;
A22: (abs x) . k0 <= (max_norm n) . x by A16, A17, A20, Def1;
(abs x) . k0 = |.(x . k0).| by A4, A16, A17, A20, VALUED_1:def 11;
then (max_norm n) . (a * x) <= |.a.| * ((max_norm n) . x) by A20, A21, A22, XREAL_1:64;
hence (max_norm n) . (a * x) = |.a.| * ((max_norm n) . x) by A19, XXREAL_0:1; :: thesis: verum

end;

thus (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) :: thesis: verum

proof

A23: dom (abs (x + y)) = dom (x + y) by VALUED_1:def 11;
consider h0 being object such that
A24: ( h0 in dom (abs (x + y)) & (max_norm n) . (x + y) = (abs (x + y)) . h0 ) by A3, FUNCT_1:def 3;
A25: h0 in Seg n by A9, A24, VALUED_1:def 11;
reconsider j0 = j0 as Nat ;
A26: (abs (x + y)) . h0 = |.((x + y) . h0).| by A24, VALUED_1:def 11
.= |.((x . h0) + (y . h0)).| by A23, A24, VALUED_1:def 1 ;
A27: |.((x . h0) + (y . h0)).| <= |.(x . h0).| + |.(y . h0).| by COMPLEX1:56;
(abs x) . h0 <= (max_norm n) . x by A7, A25, Def1;
then A28: |.(x . h0).| <= (max_norm n) . x by A4, A25, A7, VALUED_1:def 11;
(abs y) . h0 <= (max_norm n) . y by A8, A25, Def1;
then |.(y . h0).| <= (max_norm n) . y by A5, A8, A25, VALUED_1:def 11;
then |.(x . h0).| + |.(y . h0).| <= ((max_norm n) . x) + ((max_norm n) . y) by A28, XREAL_1:7;
hence (max_norm n) . (x + y) <= ((max_norm n) . x) + ((max_norm n) . y) by A24, A26, A27, XXREAL_0:2; :: thesis: verum

end;