set B = R_Normed_Algebra_of_ContinuousFunctions X;

A1: now :: thesis: for f, g being Element of (R_Normed_Algebra_of_ContinuousFunctions X) holds ||.(f * g).|| <= ||.f.|| * ||.g.||

let f, g be Element of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
reconsider f1 = f, g1 = g as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A2: ( ||.f.|| = ||.f1.|| & ||.g.|| = ||.g1.|| & ||.(f * g).|| = ||.(f1 * g1).|| ) by Lm6, Lm3;
thus ||.(f * g).|| <= ||.f.|| * ||.g.|| by A2, LOPBAN_2:def 9; :: thesis: verum

end;

A3: ||.(1. (R_Normed_Algebra_of_ContinuousFunctions X)).|| = ||.(1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)).|| by Lm8, Lm3
.= 1 by LOPBAN_2:def 10 ;

A4: now :: thesis: for a being Real
for f, g being Element of (R_Normed_Algebra_of_ContinuousFunctions X) holds a * (f * g) = f * (a * g)

let a be Real; :: thesis: for f, g being Element of (R_Normed_Algebra_of_ContinuousFunctions X) holds a * (f * g) = f * (a * g)
let f, g be Element of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: a * (f * g) = f * (a * g)
reconsider f1 = f, g1 = g as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A5: a * g1 = a * g by Lm5;
A6: f * g = f1 * g1 by Lm6;
a * (f * g) = a * (f1 * g1) by A6, Lm5;
then a * (f * g) = f1 * (a * g1) by LOPBAN_2:def 11;
hence a * (f * g) = f * (a * g) by A5, Lm6; :: thesis: verum

end;

now :: thesis: for f, g, h being Element of (R_Normed_Algebra_of_ContinuousFunctions X) holds (g + h) * f = (g * f) + (h * f)

let f, g, h be Element of (R_Normed_Algebra_of_ContinuousFunctions X); :: thesis: (g + h) * f = (g * f) + (h * f)
reconsider f1 = f, g1 = g, h1 = h as Point of (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A7: g + h = g1 + h1 by Lm4;
A8: ( g * f = g1 * f1 & h * f = h1 * f1 ) by Lm6;
thus (g + h) * f = (g1 + h1) * f1 by Lm6, A7
.= (g1 * f1) + (h1 * f1) by VECTSP_1:def 3
.= (g * f) + (h * f) by Lm4, A8 ; :: thesis: verum

end;

then R_Normed_Algebra_of_ContinuousFunctions X is left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Algebra by A1, A3, A4, LOPBAN_2:def 9, LOPBAN_2:def 10, LOPBAN_2:def 11, VECTSP_1:def 3;
hence R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like ; :: thesis: verum