let X be non empty TopSpace; :: thesis: 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r
A1: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
1_ (CAlgebra the carrier of X) = X --> 1r ;
hence 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r by A1, CC0SP1:3; :: thesis: verum