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