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

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: verumlet 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;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