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

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