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 RealLinearSpace-like by LmAlgebra; :: thesis: verum