let X be non empty set ; :: thesis: C_Normed_Algebra_of_BoundedFunctions X is ComplexAlgebra
set W = C_Normed_Algebra_of_BoundedFunctions X;
set V = C_Algebra_of_BoundedFunctions X;
C_Algebra_of_BoundedFunctions X is ComplexAlgebra ;
hence C_Normed_Algebra_of_BoundedFunctions X is ComplexAlgebra by Th14; :: thesis: verum