let X be non empty set ; :: thesis: for a being Real
for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let a be Real; :: thesis: for F, G being Point of (R_Normed_Algebra_of_BoundedFunctions X) holds
( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )
let F, G be Point of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| )

A1: now

assume A2: ||.F.|| = 0 ; :: thesis: F = 0. (R_Normed_Algebra_of_BoundedFunctions X)
F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A3: ( F = g & g | X is bounded ) ;
set z = X --> 0 ;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:58;

now

let t be Element of X; :: thesis: g . t = z . t
abs (g . t) <= ||.F.|| by A3, ThB19;
then abs (g . t) = 0 by A2, COMPLEX1:132;
hence g . t = 0 by ABSVALUE:7
.= z . t by FUNCOP_1:13 ;
:: thesis: verum

end;

then g = z by FUNCT_2:113;
hence F = 0. (R_Normed_Algebra_of_BoundedFunctions X) by A3, ThB18; :: thesis: verum

end;

A3: now

assume A4: F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ; :: thesis: ||.F.|| = 0
set z = X --> 0 ;
reconsider z = X --> 0 as Function of X,REAL by FUNCOP_1:58;
F in BoundedFunctions X ;
then consider g being Function of X,REAL such that
A41: ( F = g & g | X is bounded ) ;
A5: z = g by A41, A4, ThB18;

A6: now

let r be Real; :: thesis: ( r in PreNorms g implies ( 0 <= r & r <= 0 ) )
assume A7: r in PreNorms g ; :: thesis: ( 0 <= r & r <= 0 )
consider t being Element of X such that
A8: r = abs (g . t) by A7;
abs (g . t) = abs 0 by A5, FUNCOP_1:13
.= 0 by ABSVALUE:7 ;
hence ( 0 <= r & r <= 0 ) by A8; :: thesis: verum

end;

A9: ( not PreNorms g is empty & PreNorms g is bounded_above ) by A41, ThB13;
consider r0 being set such that
A10: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A10;
A11: 0 <= r0 by A6, A10;
( ( for s being real number st s in PreNorms g holds
s <= 0 ) implies sup (PreNorms g) <= 0 ) by SEQ_4:62;
then sup (PreNorms g) = 0 by A6, A9, A10, A11, SEQ_4:def 4;
hence ||.F.|| = 0 by A41, ThB17; :: thesis: verum

end;

A12: ||.(a * F).|| = (abs a) * ||.F.||

proof

F in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A121: ( f1 = F & f1 | X is bounded ) ;
a * F in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A122: ( h1 = a * F & h1 | X is bounded ) ;

A13: now

let t be Element of X; :: thesis: abs (h1 . t) <= (abs a) * ||.F.||
abs (h1 . t) = abs (a * (f1 . t)) by A121, A122, ThB23;
then A15: abs (h1 . t) = (abs a) * (abs (f1 . t)) by COMPLEX1:151;
0 <= abs a by COMPLEX1:132;
hence abs (h1 . t) <= (abs a) * ||.F.|| by A15, A121, ThB19, XREAL_1:66; :: thesis: verum

end;

A17: now

let r be Real; :: thesis: ( r in PreNorms h1 implies r <= (abs a) * ||.F.|| )
assume r in PreNorms h1 ; :: thesis: r <= (abs a) * ||.F.||
then ex t being Element of X st r = abs (h1 . t) ;
hence r <= (abs a) * ||.F.|| by A13; :: thesis: verum

end;

( ( for s being real number st s in PreNorms h1 holds
s <= (abs a) * ||.F.|| ) implies sup (PreNorms h1) <= (abs a) * ||.F.|| ) by SEQ_4:62;
then A21: ||.(a * F).|| <= (abs a) * ||.F.|| by A17, A122, ThB17;

per cases ( a <> 0 or a = 0 ) ;

suppose A22: a <> 0 ; :: thesis: ||.(a * F).|| = (abs a) * ||.F.||

then A31: abs a <> 0 by COMPLEX1:133;

A23: now

let t be Element of X; :: thesis: abs (f1 . t) <= ((abs a) " ) * ||.(a * F).||
h1 . t = a * (f1 . t) by A121, A122, ThB23;
then (a " ) * (h1 . t) = ((a " ) * a) * (f1 . t) ;
then A24: (a " ) * (h1 . t) = 1 * (f1 . t) by A22, XCMPLX_0:def 7;
A25: abs ((a " ) * (h1 . t)) = (abs (a " )) * (abs (h1 . t)) by COMPLEX1:151;
A27: 0 <= abs (a " ) by COMPLEX1:132;
abs (a " ) = abs (1 / a) ;
then abs (a " ) = 1 / (abs a) by ABSVALUE:15;
hence abs (f1 . t) <= ((abs a) " ) * ||.(a * F).|| by A24, A25, A122, ThB19, A27, XREAL_1:66; :: thesis: verum

end;

A28: now

let r be Real; :: thesis: ( r in PreNorms f1 implies r <= ((abs a) " ) * ||.(a * F).|| )
assume r in PreNorms f1 ; :: thesis: r <= ((abs a) " ) * ||.(a * F).||
then ex t being Element of X st r = abs (f1 . t) ;
hence r <= ((abs a) " ) * ||.(a * F).|| by A23; :: thesis: verum

end;

A32: ( ( for s being real number st s in PreNorms f1 holds
s <= ((abs a) " ) * ||.(a * F).|| ) implies sup (PreNorms f1) <= ((abs a) " ) * ||.(a * F).|| ) by SEQ_4:62;
A33: ||.F.|| <= ((abs a) " ) * ||.(a * F).|| by A28, A32, A121, ThB17;
0 <= abs a by COMPLEX1:132;
then (abs a) * ||.F.|| <= (abs a) * (((abs a) " ) * ||.(a * F).||) by A33, XREAL_1:66;
then (abs a) * ||.F.|| <= ((abs a) * ((abs a) " )) * ||.(a * F).|| ;
then (abs a) * ||.F.|| <= 1 * ||.(a * F).|| by A31, XCMPLX_0:def 7;
hence ||.(a * F).|| = (abs a) * ||.F.|| by A21, XXREAL_0:1; :: thesis: verum

end;

suppose A34: a = 0 ; :: thesis: ||.(a * F).|| = (abs a) * ||.F.||

reconsider fz = F as VECTOR of (R_Algebra_of_BoundedFunctions X) ;
a * fz = (a + a) * fz by A34
.= (a * fz) + (a * fz) by FUNCSDOM:def 20 ;
then 0. (R_Algebra_of_BoundedFunctions X) = (- (a * fz)) + ((a * fz) + (a * fz)) by VECTSP_1:63;
then 0. (R_Algebra_of_BoundedFunctions X) = ((- (a * fz)) + (a * fz)) + (a * fz) by RLVECT_1:def 6;
then 0. (R_Algebra_of_BoundedFunctions X) = (0. (R_Algebra_of_BoundedFunctions X)) + (a * fz) by VECTSP_1:63;
then A35: a * F = 0. (R_Normed_Algebra_of_BoundedFunctions X) by RLVECT_1:10;
(abs a) * ||.F.|| = 0 * ||.F.|| by A34, ABSVALUE:7;
hence ||.(a * F).|| = (abs a) * ||.F.|| by A35, ThB21; :: thesis: verum

end;

end;

end;

||.(F + G).|| <= ||.F.|| + ||.G.||

proof

F in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A361: ( f1 = F & f1 | X is bounded ) ;
G in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A362: ( g1 = G & g1 | X is bounded ) ;
F + G in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A363: ( h1 = F + G & h1 | X is bounded ) ;

A36: now

let t be Element of X; :: thesis: abs (h1 . t) <= ||.F.|| + ||.G.||
A37: abs (h1 . t) = abs ((f1 . t) + (g1 . t)) by A361, A362, A363, ThB22;
A38: abs ((f1 . t) + (g1 . t)) <= (abs (f1 . t)) + (abs (g1 . t)) by COMPLEX1:142;
( abs (f1 . t) <= ||.F.|| & abs (g1 . t) <= ||.G.|| ) by A361, A362, ThB19;
then (abs (f1 . t)) + (abs (g1 . t)) <= ||.F.|| + ||.G.|| by XREAL_1:9;
hence abs (h1 . t) <= ||.F.|| + ||.G.|| by A37, A38, XXREAL_0:2; :: thesis: verum

end;

A40: now

let r be Real; :: thesis: ( r in PreNorms h1 implies r <= ||.F.|| + ||.G.|| )
assume r in PreNorms h1 ; :: thesis: r <= ||.F.|| + ||.G.||
then ex t being Element of X st r = abs (h1 . t) ;
hence r <= ||.F.|| + ||.G.|| by A36; :: thesis: verum

end;

( ( for s being real number st s in PreNorms h1 holds
s <= ||.F.|| + ||.G.|| ) implies sup (PreNorms h1) <= ||.F.|| + ||.G.|| ) by SEQ_4:62;
hence ||.(F + G).|| <= ||.F.|| + ||.G.|| by A40, A363, ThB17; :: thesis: verum

end;

hence ( ( ||.F.|| = 0 implies F = 0. (R_Normed_Algebra_of_BoundedFunctions X) ) & ( F = 0. (R_Normed_Algebra_of_BoundedFunctions X) implies ||.F.|| = 0 ) & ||.(a * F).|| = (abs a) * ||.F.|| & ||.(F + G).|| <= ||.F.|| + ||.G.|| ) by A1, A3, A12; :: thesis: verum