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

let v be VECTOR of (C_Algebra_of_ContinuousFunctions X); :: thesis: 1r * v = v
reconsider v1 = v as VECTOR of (CAlgebra the carrier of X) by TARSKI:def 3;
C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
then 1r * v = 1r * v1 by CC0SP1:3;
hence 1r * v = v by CFUNCDOM:12; :: thesis: verum

end;

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