set B = C_Normed_Algebra_of_ContinuousFunctions X;
A1: now :: thesis: for f, g being Element of (C_Normed_Algebra_of_ContinuousFunctions X) holds ||.(f * g).|| <= ||.f.|| * ||.g.||
let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: ||.(f * g).|| <= ||.f.|| * ||.g.||
reconsider f1 = f, g1 = g as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A2: ( ||.f.|| = ||.f1.|| & ||.g.|| = ||.g1.|| & ||.(f * g).|| = ||.(f1 * g1).|| ) by Lm6, Lm3;
C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_1 by CC0SP1:28;
hence ||.(f * g).|| <= ||.f.|| * ||.g.|| by A2, CLOPBAN2:def 9; :: thesis: verum
end;
A3: C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_2 by CC0SP1:28;
A4: ||.(1. (C_Normed_Algebra_of_ContinuousFunctions X)).|| = ||.(1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)).|| by Lm8, Lm3
.= 1 by A3, CLOPBAN2:def 10 ;
A5: now :: thesis: for a being Complex
for f, g being Element of (C_Normed_Algebra_of_ContinuousFunctions X) holds a * (f * g) = f * (a * g)
let a be Complex; :: thesis: for f, g being Element of (C_Normed_Algebra_of_ContinuousFunctions X) holds a * (f * g) = f * (a * g)
let f, g be Element of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: a * (f * g) = f * (a * g)
reconsider f1 = f, g1 = g as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A6: a * g1 = a * g by Lm5;
A7: f * g = f1 * g1 by Lm6;
A8: C_Normed_Algebra_of_BoundedFunctions the carrier of X is Banach_Algebra-like_3 by CC0SP1:28;
a * (f * g) = a * (f1 * g1) by A7, Lm5;
then a * (f * g) = f1 * (a * g1) by A8, CLOPBAN2:def 11;
hence a * (f * g) = f * (a * g) by A6, Lm6; :: thesis: verum
end;
now :: thesis: for f, g, h being Element of (C_Normed_Algebra_of_ContinuousFunctions X) holds (g + h) * f = (g * f) + (h * f)
let f, g, h be Element of (C_Normed_Algebra_of_ContinuousFunctions X); :: thesis: (g + h) * f = (g * f) + (h * f)
reconsider f1 = f, g1 = g, h1 = h as Point of (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A9: g + h = g1 + h1 by Lm4;
A10: ( g * f = g1 * f1 & h * f = h1 * f1 ) by Lm6;
A11: C_Normed_Algebra_of_BoundedFunctions the carrier of X is left-distributive by CC0SP1:28;
thus (g + h) * f = (g1 + h1) * f1 by Lm6, A9
.= (g1 * f1) + (h1 * f1) by A11, VECTSP_1:def 3
.= (g * f) + (h * f) by Lm4, A10 ; :: thesis: verum
end;
then C_Normed_Algebra_of_ContinuousFunctions X is left-distributive left_unital complete Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Normed_Complex_Algebra by A1, A4, A5, CLOPBAN2:def 9, CLOPBAN2:def 10, CLOPBAN2:def 11, VECTSP_1:def 3;
hence C_Normed_Algebra_of_ContinuousFunctions X is Banach_Algebra-like ; :: thesis: verum