for v being VECTOR of (R_Normed_Algebra_of_ContinuousFunctions X) holds 1 * v = v by FUNCSDOM23;
hence ( 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 scalar-unital ) by RLVECT_1:def 11; :: thesis: verum