set B = R_Normed_Algebra_of_BoundedFunctions X;
thus R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_1 :: thesis: ( R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_2 & R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedFunctions X is left-distributive & R_Normed_Algebra_of_BoundedFunctions X is left_unital )

proof

let f, g be Element of (R_Normed_Algebra_of_BoundedFunctions X); :: according to LOPBAN_2:def 9 :: thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A1: f1 = f and
A2: f1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A3: g1 = g and
A4: g1 | X is bounded ;
A5: ( not PreNorms g1 is empty & PreNorms g1 is bounded_above ) by A4, Th17;
f * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A6: h1 = f * g and
A7: h1 | X is bounded ;
A8: ( not PreNorms f1 is empty & PreNorms f1 is bounded_above ) by A2, Th17;

now :: thesis: for s being Real st s in PreNorms h1 holds
s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))

let s be Real; :: thesis: ( s in PreNorms h1 implies s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) )
assume s in PreNorms h1 ; :: thesis: s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1))
then consider t being Element of X such that
A9: s = |.(h1 . t).| ;
|.(g1 . t).| in PreNorms g1 ;
then A10: |.(g1 . t).| <= upper_bound (PreNorms g1) by A5, SEQ_4:def 1;
|.(f1 . t).| in PreNorms f1 ;
then A11: |.(f1 . t).| <= upper_bound (PreNorms f1) by A8, SEQ_4:def 1;
0 <= |.(f1 . t).| by COMPLEX1:46;
then 0 <= upper_bound (PreNorms f1) by A11;
then A12: (upper_bound (PreNorms f1)) * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A10, XREAL_1:64;
0 <= |.(g1 . t).| by COMPLEX1:46;
then A13: |.(f1 . t).| * |.(g1 . t).| <= (upper_bound (PreNorms f1)) * |.(g1 . t).| by A11, XREAL_1:64;
|.(h1 . t).| = |.((f1 . t) * (g1 . t)).| by A1, A3, A6, Th31;
then |.(h1 . t).| = |.(f1 . t).| * |.(g1 . t).| by COMPLEX1:65;
hence s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A9, A13, A12, XXREAL_0:2; :: thesis: verum

end;

then A14: upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by SEQ_4:45;
A15: ||.g.|| = upper_bound (PreNorms g1) by A3, A4, Th20;
||.f.|| = upper_bound (PreNorms f1) by A1, A2, Th20;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A6, A7, A15, A14, Th20; :: thesis: verum

end;

1. (R_Normed_Algebra_of_BoundedFunctions X) in BoundedFunctions X ;
then consider ONE being Function of X,REAL such that
A16: ONE = 1. (R_Normed_Algebra_of_BoundedFunctions X) and
A17: ONE | X is bounded ;
1. (R_Normed_Algebra_of_BoundedFunctions X) = 1_ (R_Algebra_of_BoundedFunctions X) ;
then A18: 1. (R_Normed_Algebra_of_BoundedFunctions X) = X --> 1 by Th16;
for s being object holds
( s in PreNorms ONE iff s = 1 )

proof

set t = the Element of X;
let s be object ; :: thesis: ( s in PreNorms ONE iff s = 1 )

hereby :: thesis: ( s = 1 implies s in PreNorms ONE )

assume s in PreNorms ONE ; :: thesis: s = 1
then consider t being Element of X such that
A20: s = |.(ONE . t).| ;
A21: s = |.((X --> 1) . t).| by A16, A18, A20;
thus s = 1 by A21, COMPLEX1:48; :: thesis: verum

end;

assume s = 1 ; :: thesis: s in PreNorms ONE
then s = |.((X --> 1) . the Element of X).| by COMPLEX1:48;
hence s in PreNorms ONE by A16, A18; :: thesis: verum

end;

then PreNorms ONE = {1} by TARSKI:def 1;
then upper_bound (PreNorms ONE) = 1 by SEQ_4:9;
then ||.(1. (R_Normed_Algebra_of_BoundedFunctions X)).|| = 1 by A16, A17, Th20;
hence R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_2 ; :: thesis: ( R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_3 & R_Normed_Algebra_of_BoundedFunctions X is left-distributive & R_Normed_Algebra_of_BoundedFunctions X is left_unital )
thus R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra-like_3 :: thesis: ( R_Normed_Algebra_of_BoundedFunctions X is left-distributive & R_Normed_Algebra_of_BoundedFunctions X is left_unital )

proof

let a be Real; :: according to LOPBAN_2:def 11 :: thesis: for b₁, b₂ being Element of the carrier of (R_Normed_Algebra_of_BoundedFunctions X) holds a * (b₁ * b₂) = b₁ * (a * b₂)
let f, g be Element of (R_Normed_Algebra_of_BoundedFunctions X); :: thesis: a * (f * g) = f * (a * g)
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A22: f1 = f and
f1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A23: g1 = g and
g1 | X is bounded ;
a * (f * g) in BoundedFunctions X ;
then consider h3 being Function of X,REAL such that
A24: h3 = a * (f * g) and
h3 | X is bounded ;
f * g in BoundedFunctions X ;
then consider h2 being Function of X,REAL such that
A25: h2 = f * g and
h2 | X is bounded ;
a * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A26: h1 = a * g and
h1 | X is bounded ;

now :: thesis: for x being Element of X holds h3 . x = (f1 . x) * (h1 . x)

let x be Element of X; :: thesis: h3 . x = (f1 . x) * (h1 . x)
h3 . x = a * (h2 . x) by A25, A24, Th30;
then h3 . x = a * ((f1 . x) * (g1 . x)) by A22, A23, A25, Th31;
then h3 . x = (f1 . x) * (a * (g1 . x)) ;
hence h3 . x = (f1 . x) * (h1 . x) by A23, A26, Th30; :: thesis: verum

end;

hence a * (f * g) = f * (a * g) by A22, A26, A24, Th31; :: thesis: verum

end;

thus R_Normed_Algebra_of_BoundedFunctions X is left-distributive :: thesis: R_Normed_Algebra_of_BoundedFunctions X is left_unital

proof

let f, g, h be Element of (R_Normed_Algebra_of_BoundedFunctions X); :: according to VECTSP_1:def 3 :: thesis: (g + h) * f = (g * f) + (h * f)
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A27: f1 = f and
f1 | X is bounded ;
h in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A28: h1 = h and
h1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A29: g1 = g and
g1 | X is bounded ;
(g + h) * f in BoundedFunctions X ;
then consider F1 being Function of X,REAL such that
A30: F1 = (g + h) * f and
F1 | X is bounded ;
h * f in BoundedFunctions X ;
then consider hf1 being Function of X,REAL such that
A31: hf1 = h * f and
hf1 | X is bounded ;
g * f in BoundedFunctions X ;
then consider gf1 being Function of X,REAL such that
A32: gf1 = g * f and
gf1 | X is bounded ;
g + h in BoundedFunctions X ;
then consider gPh1 being Function of X,REAL such that
A33: gPh1 = g + h and
gPh1 | X is bounded ;

now :: thesis: for x being Element of X holds F1 . x = (gf1 . x) + (hf1 . x)

let x be Element of X; :: thesis: F1 . x = (gf1 . x) + (hf1 . x)
F1 . x = (gPh1 . x) * (f1 . x) by A27, A33, A30, Th31;
then F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x) by A29, A28, A33, Th29;
then F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)) ;
then F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x)) by A27, A29, A32, Th31;
hence F1 . x = (gf1 . x) + (hf1 . x) by A27, A28, A31, Th31; :: thesis: verum

end;

hence (g + h) * f = (g * f) + (h * f) by A32, A31, A30, Th29; :: thesis: verum

end;

thus for f being Element of (R_Normed_Algebra_of_BoundedFunctions X) holds (1. (R_Normed_Algebra_of_BoundedFunctions X)) * f = f by Lm3; :: according to VECTSP_1:def 8 :: thesis: verum