let X be non empty TopSpace; :: thesis: 0. (R_Algebra_of_ContinuousFunctions X) = X --> 0
A1: R_Algebra_of_ContinuousFunctions X is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
0. (RAlgebra the carrier of X) = X --> 0 ;
hence 0. (R_Algebra_of_ContinuousFunctions X) = X --> 0 by A1, C0SP1:8; :: thesis: verum