let X be non empty compact TopSpace; :: thesis: C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra
1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1_ (C_Algebra_of_ContinuousFunctions X) ;
hence C_Normed_Algebra_of_ContinuousFunctions X is ComplexAlgebra by CC0SP1:14; :: thesis: verum