1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1_ (R_Algebra_of_ContinuousFunctions X) ;
hence ( R_Normed_Algebra_of_ContinuousFunctions X is Abelian & R_Normed_Algebra_of_ContinuousFunctions X is add-associative & R_Normed_Algebra_of_ContinuousFunctions X is right_zeroed & R_Normed_Algebra_of_ContinuousFunctions X is right_complementable & R_Normed_Algebra_of_ContinuousFunctions X is commutative & R_Normed_Algebra_of_ContinuousFunctions X is associative & R_Normed_Algebra_of_ContinuousFunctions X is right_unital & R_Normed_Algebra_of_ContinuousFunctions X is right-distributive & R_Normed_Algebra_of_ContinuousFunctions X is vector-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Normed_Algebra_of_ContinuousFunctions X is scalar-associative & R_Normed_Algebra_of_ContinuousFunctions X is vector-associative ) by Th10; :: thesis: verum