now :: thesis: for v being VECTOR of (R_Algebra_of_Ck_Functions (k,X)) holds 1 * v = v

let v be VECTOR of (R_Algebra_of_Ck_Functions (k,X)); :: thesis: 1 * v = v
reconsider v1 = v as VECTOR of (RAlgebra X) by TARSKI:def 3;
1 * v = 1 * v1 by C0SP1:8;
hence 1 * v = v by FUNCSDOM:12; :: thesis: verum

end;

hence ( R_Algebra_of_Ck_Functions (k,X) is Abelian & R_Algebra_of_Ck_Functions (k,X) is add-associative & R_Algebra_of_Ck_Functions (k,X) is right_zeroed & R_Algebra_of_Ck_Functions (k,X) is right_complementable & R_Algebra_of_Ck_Functions (k,X) is vector-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is scalar-unital & R_Algebra_of_Ck_Functions (k,X) is commutative & R_Algebra_of_Ck_Functions (k,X) is associative & R_Algebra_of_Ck_Functions (k,X) is right_unital & R_Algebra_of_Ck_Functions (k,X) is right-distributive & R_Algebra_of_Ck_Functions (k,X) is scalar-associative & R_Algebra_of_Ck_Functions (k,X) is vector-associative ) ; :: thesis: verum