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