let X be non empty set ; :: thesis:
set B = R_Normed_Algebra_of_BoundedFunctions X;
set X1 = BoundedFunctions X;
reconsider B = R_Normed_Algebra_of_BoundedFunctions X as non empty Normed_Algebra by LmAlgebra4;

A1: now

let f, g be Element of B; :: thesis:
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A01: ( f1 = f & f1 | X is bounded ) ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A02: ( g1 = g & g1 | X is bounded ) ;
f * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A03: ( h1 = f * g & h1 | X is bounded ) ;
A04: ( not PreNorms f1 is empty & PreNorms f1 is bounded_above & not PreNorms g1 is empty & PreNorms g1 is bounded_above & not PreNorms h1 is empty & PreNorms h1 is bounded_above ) by A01, A02, A03, ThB13;
B01: ||.f.|| = sup (PreNorms f1) by A01, ThB17;
B02: ||.g.|| = sup (PreNorms g1) by A02, ThB17;

now

let s be real number ; :: thesis:
assume s in PreNorms h1 ; :: thesis:
then consider t being Element of X such that
E1: s = abs (h1 . t) ;
abs (h1 . t) = abs ((f1 . t) * (g1 . t)) by A01, A02, A03, ThB23a;
then E2: abs (h1 . t) = (abs (f1 . t)) * (abs (g1 . t)) by COMPLEX1:151;
E3: ( 0 <= abs (f1 . t) & 0 <= abs (g1 . t) ) by COMPLEX1:132;
abs (f1 . t) in PreNorms f1 ;
then E4: abs (f1 . t) <= sup (PreNorms f1) by A04, SEQ_4:def 4;
then E5: (abs (f1 . t)) * (abs (g1 . t)) <= (sup (PreNorms f1)) * (abs (g1 . t)) by E3, XREAL_1:66;
E6: 0 <= sup (PreNorms f1) by E4, COMPLEX1:132;
abs (g1 . t) in PreNorms g1 ;
then abs (g1 . t) <= sup (PreNorms g1) by A04, SEQ_4:def 4;
then (sup (PreNorms f1)) * (abs (g1 . t)) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by E6, XREAL_1:66;
hence s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by E1, E2, E5, XXREAL_0:2; :: thesis:

end;

then upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by SEQ_4:62;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by B01, B02, A03, ThB17; :: thesis:

end;

1. B in BoundedFunctions X ;
then consider ONE being Function of X,REAL such that
A21: ( ONE = 1. B & ONE | X is bounded ) ;
1. B = 1_ (R_Algebra_of_BoundedFunctions X) ;
then A22: 1. B = X --> 1 by ThB12One;
for s being set holds
( s in PreNorms ONE iff s = 1 )

proof

let s be set ; :: thesis:

hereby :: thesis:

assume s in PreNorms ONE ; :: thesis:
then consider t being Element of X such that
A23: s = abs ((X --> 1) . t) by A21, A22;
(X --> 1) . t = 1 by FUNCOP_1:13;
hence s = 1 by A23, COMPLEX1:134; :: thesis:

end;

assume A24: s = 1 ; :: thesis:
consider t being Element of X;
(X --> 1) . t = 1 by FUNCOP_1:13;
then s = abs ((X --> 1) . t) by A24, COMPLEX1:134;
hence s in PreNorms ONE by A21, A22; :: thesis:

end;

then PreNorms ONE = {1} by TARSKI:def 1;
then sup (PreNorms ONE) = 1 by SEQ_4:22;
then A2: ||.(1. B).|| = 1 by A21, ThB17;

A3: now

let a be Real; :: thesis:
let f, g be Element of B; :: thesis:
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A31: ( f1 = f & f1 | X is bounded ) ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A32: ( g1 = g & g1 | X is bounded ) ;
a * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A33: ( h1 = a * g & h1 | X is bounded ) ;
f * g in BoundedFunctions X ;
then consider h2 being Function of X,REAL such that
A34: ( h2 = f * g & h2 | X is bounded ) ;
a * (f * g) in BoundedFunctions X ;
then consider h3 being Function of X,REAL such that
A35: ( h3 = a * (f * g) & h3 | X is bounded ) ;

now

let x be Element of X; :: thesis:
h3 . x = a * (h2 . x) by A34, A35, ThB23;
then h3 . x = a * ((f1 . x) * (g1 . x)) by A31, A32, A34, ThB23a;
then h3 . x = (f1 . x) * (a * (g1 . x)) ;
hence h3 . x = (f1 . x) * (h1 . x) by A32, A33, ThB23; :: thesis:

end;

hence a * (f * g) = f * (a * g) by A31, A33, A35, ThB23a; :: thesis:

end;

A4: now

let f, g, h be Element of B; :: thesis:
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A41: ( f1 = f & f1 | X is bounded ) ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A42: ( g1 = g & g1 | X is bounded ) ;
h in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A43: ( h1 = h & h1 | X is bounded ) ;
g + h in BoundedFunctions X ;
then consider gPh1 being Function of X,REAL such that
A44: ( gPh1 = g + h & gPh1 | X is bounded ) ;
g * f in BoundedFunctions X ;
then consider gf1 being Function of X,REAL such that
A45: ( gf1 = g * f & gf1 | X is bounded ) ;
h * f in BoundedFunctions X ;
then consider hf1 being Function of X,REAL such that
A46: ( hf1 = h * f & hf1 | X is bounded ) ;
(g + h) * f in BoundedFunctions X ;
then consider F1 being Function of X,REAL such that
A47: ( F1 = (g + h) * f & F1 | X is bounded ) ;

now

let x be Element of X; :: thesis:
F1 . x = (gPh1 . x) * (f1 . x) by A44, A41, A47, ThB23a;
then F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x) by A42, A43, A44, ThB22;
then F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)) ;
then F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x)) by A41, A42, A45, ThB23a;
hence F1 . x = (gf1 . x) + (hf1 . x) by A41, A43, A46, ThB23a; :: thesis:

end;

hence (g + h) * f = (g * f) + (h * f) by A45, A46, A47, ThB22; :: thesis:

end;

A5: for f being Element of B holds (1. B) * f = f by UNITAL;
B is complete left-distributive left_unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Algebra by A1, A2, A3, A4, A5, LOPBAN_2:def 9, LOPBAN_2:def 10, LOPBAN_2:def 11, VECTSP_1:def 12, VECTSP_1:def 19;
hence R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra ; :: thesis: