now :: thesis: for v being VECTOR of (R_Algebra_of_ContinuousFunctions X) holds 1 * v = v

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:12; :: 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 vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is scalar-unital & 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 vector-distributive & R_Algebra_of_ContinuousFunctions X is scalar-distributive & R_Algebra_of_ContinuousFunctions X is scalar-associative & R_Algebra_of_ContinuousFunctions X is vector-associative ) by C0SP1:6; :: thesis: verum