A1: R_Algebra_of_ContinuousFunctions X is Algebra by C0SP1:6;

now

let v be VECTOR of (R_Algebra_of_ContinuousFunctions X); :: thesis: 1 * v = v
reconsider v1 = v as VECTOR of (RAlgebra the carrier of X) by TARSKI:def 3;
R_Algebra_of_ContinuousFunctions X is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
then 1 * v = 1 * v1 by C0SP1:8;
hence 1 * v = v by FUNCSDOM:23; :: thesis: verum

end;

hence ( R_Algebra_of_ContinuousFunctions X is Abelian & R_Algebra_of_ContinuousFunctions X is add-associative & R_Algebra_of_ContinuousFunctions X is right_zeroed & R_Algebra_of_ContinuousFunctions X is right_complementable & R_Algebra_of_ContinuousFunctions X is RealLinearSpace-like & R_Algebra_of_ContinuousFunctions X is commutative & R_Algebra_of_ContinuousFunctions X is associative & R_Algebra_of_ContinuousFunctions X is right_unital & R_Algebra_of_ContinuousFunctions X is right-distributive & R_Algebra_of_ContinuousFunctions X is Algebra-like ) by A1, LmAlgebra; :: thesis: verum