set B = R_Normed_Algebra_of_ContinuousFunctions X;
set X1 = ContinuousFunctions X;

A1: now

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 LMX01;
A2: ( ||.f.|| = ||.f1.|| & ||.g.|| = ||.g1.|| & ||.(f * g).|| = ||.(f1 * g1).|| ) by LMX05, LMX02;
R_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_1 by C0SP1:38;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A2, LOPBAN_2:def 9; :: thesis: verum

end;

A3: R_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_2 by C0SP1:38;
A4: ||.(1. (R_Normed_Algebra_of_ContinuousFunctions X)).|| = ||.(1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)).|| by LMX07, LMX02
.= 1 by A3, LOPBAN_2:def 10 ;

A5: now

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 LMX01;
A6: a * g1 = a * g by LMX04;
A7: f * g = f1 * g1 by LMX05;
A8: R_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_3 by C0SP1:38;
a * (f * g) = a * (f1 * g1) by A7, LMX04;
then a * (f * g) = f1 * (a * g1) by A8, LOPBAN_2:def 11;
hence a * (f * g) = f * (a * g) by A6, LMX05; :: thesis: verum

end;

now

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 LMX01;
A10: g + h = g1 + h1 by LMX03;
A11: ( g * f = g1 * f1 & h * f = h1 * f1 ) by LMX05;
A12: R_Normed_Algebra_of_BoundedFunctions the carrier of X is left-distributive by C0SP1:38;
thus (g + h) * f = (g1 + h1) * f1 by LMX05, A10
.= (g1 * f1) + (h1 * f1) by A12, VECTSP_1:def 12
.= (g * f) + (h * f) by LMX03, A11 ; :: 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, A4, A5, LOPBAN_2:def 9, LOPBAN_2:def 10, LOPBAN_2:def 11, VECTSP_1:def 12;
hence R_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like ; :: thesis: verum