let X be non empty set ; :: thesis: R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra
set B = R_Normed_Algebra_of_BoundedFunctions X;
reconsider B = R_Normed_Algebra_of_BoundedFunctions X as Normed_Algebra by Th23;
1. B in BoundedFunctions X ;
then consider ONE being Function of X,REAL such that
A1: ONE = 1. B and
A2: ONE | X is bounded ;
1. B = 1_ (R_Algebra_of_BoundedFunctions X) ;
then A3: 1. B = X --> 1 by Th16;
for s being set holds
( s in PreNorms ONE iff s = 1 )

proof

set t = the Element of X;
let s be set ; :: thesis: ( s in PreNorms ONE iff s = 1 )
A4: (X --> 1) . the Element of X = 1 by FUNCOP_1:7;

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
A5: s = abs ((X --> 1) . t) by A1, A3;
(X --> 1) . t = 1 by FUNCOP_1:7;
hence s = 1 by A5, COMPLEX1:48; :: thesis: verum

end;

assume s = 1 ; :: thesis: s in PreNorms ONE
then s = abs ((X --> 1) . the Element of X) by A4, COMPLEX1:48;
hence s in PreNorms ONE by A1, A3; :: thesis: verum

end;

then PreNorms ONE = {1} by TARSKI:def 1;
then upper_bound (PreNorms ONE) = 1 by SEQ_4:9;
then A6: ||.(1. B).|| = 1 by A1, A2, Th21;

A7: now

let a be Real; :: thesis: for f, g being Element of B holds a * (f * g) = f * (a * g)
let f, g be Element of B; :: thesis: a * (f * g) = f * (a * g)
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A8: f1 = f and
f1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A9: g1 = g and
g1 | X is bounded ;
a * (f * g) in BoundedFunctions X ;
then consider h3 being Function of X,REAL such that
A10: h3 = a * (f * g) and
h3 | X is bounded ;
f * g in BoundedFunctions X ;
then consider h2 being Function of X,REAL such that
A11: h2 = f * g and
h2 | X is bounded ;
a * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A12: h1 = a * g and
h1 | X is bounded ;

now

let x be Element of X; :: thesis: h3 . x = (f1 . x) * (h1 . x)
h3 . x = a * (h2 . x) by A11, A10, Th31;
then h3 . x = a * ((f1 . x) * (g1 . x)) by A8, A9, A11, Th32;
then h3 . x = (f1 . x) * (a * (g1 . x)) ;
hence h3 . x = (f1 . x) * (h1 . x) by A9, A12, Th31; :: thesis: verum

end;

hence a * (f * g) = f * (a * g) by A8, A12, A10, Th32; :: thesis: verum

end;

A13: now

let f, g be Element of B; :: thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A14: f1 = f and
A15: f1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A16: g1 = g and
A17: g1 | X is bounded ;
A18: ( not PreNorms g1 is empty & PreNorms g1 is bounded_above ) by A17, Th17;
f * g in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A19: h1 = f * g and
A20: h1 | X is bounded ;
A21: ( not PreNorms f1 is empty & PreNorms f1 is bounded_above ) by A15, Th17;

now

let s be real number ; :: 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
A22: s = abs (h1 . t) ;
abs (g1 . t) in PreNorms g1 ;
then A23: abs (g1 . t) <= upper_bound (PreNorms g1) by A18, SEQ_4:def 1;
abs (f1 . t) in PreNorms f1 ;
then A24: abs (f1 . t) <= upper_bound (PreNorms f1) by A21, SEQ_4:def 1;
then 0 <= upper_bound (PreNorms f1) by COMPLEX1:46;
then A25: (upper_bound (PreNorms f1)) * (abs (g1 . t)) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A23, XREAL_1:64;
0 <= abs (g1 . t) by COMPLEX1:46;
then A26: (abs (f1 . t)) * (abs (g1 . t)) <= (upper_bound (PreNorms f1)) * (abs (g1 . t)) by A24, XREAL_1:64;
abs (h1 . t) = abs ((f1 . t) * (g1 . t)) by A14, A16, A19, Th32;
then abs (h1 . t) = (abs (f1 . t)) * (abs (g1 . t)) by COMPLEX1:65;
hence s <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by A22, A26, A25, XXREAL_0:2; :: thesis: verum

end;

then A27: upper_bound (PreNorms h1) <= (upper_bound (PreNorms f1)) * (upper_bound (PreNorms g1)) by SEQ_4:45;
A28: ||.g.|| = upper_bound (PreNorms g1) by A16, A17, Th21;
||.f.|| = upper_bound (PreNorms f1) by A14, A15, Th21;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A19, A20, A28, A27, Th21; :: thesis: verum

end;

A29: now

let f, g, h be Element of B; :: thesis: (g + h) * f = (g * f) + (h * f)
f in BoundedFunctions X ;
then consider f1 being Function of X,REAL such that
A30: f1 = f and
f1 | X is bounded ;
h in BoundedFunctions X ;
then consider h1 being Function of X,REAL such that
A31: h1 = h and
h1 | X is bounded ;
g in BoundedFunctions X ;
then consider g1 being Function of X,REAL such that
A32: g1 = g and
g1 | X is bounded ;
(g + h) * f in BoundedFunctions X ;
then consider F1 being Function of X,REAL such that
A33: F1 = (g + h) * f and
F1 | X is bounded ;
h * f in BoundedFunctions X ;
then consider hf1 being Function of X,REAL such that
A34: hf1 = h * f and
hf1 | X is bounded ;
g * f in BoundedFunctions X ;
then consider gf1 being Function of X,REAL such that
A35: gf1 = g * f and
gf1 | X is bounded ;
g + h in BoundedFunctions X ;
then consider gPh1 being Function of X,REAL such that
A36: gPh1 = g + h and
gPh1 | X is bounded ;

now

let x be Element of X; :: thesis: F1 . x = (gf1 . x) + (hf1 . x)
F1 . x = (gPh1 . x) * (f1 . x) by A30, A36, A33, Th32;
then F1 . x = ((g1 . x) + (h1 . x)) * (f1 . x) by A32, A31, A36, Th30;
then F1 . x = ((g1 . x) * (f1 . x)) + ((h1 . x) * (f1 . x)) ;
then F1 . x = (gf1 . x) + ((h1 . x) * (f1 . x)) by A30, A32, A35, Th32;
hence F1 . x = (gf1 . x) + (hf1 . x) by A30, A31, A34, Th32; :: thesis: verum

end;

hence (g + h) * f = (g * f) + (h * f) by A35, A34, A33, Th30; :: thesis: verum

end;

for f being Element of B holds (1. B) * f = f by Lm4;
then B is complete left-distributive left_unital Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Algebra by A13, A6, A7, A29, LOPBAN_2:def 9, LOPBAN_2:def 10, LOPBAN_2:def 11, VECTSP_1:def 3, VECTSP_1:def 8;
hence R_Normed_Algebra_of_BoundedFunctions X is Banach_Algebra ; :: thesis: verum