let X be non empty compact TopSpace; :: thesis: 0. (R_Normed_Algebra_of_ContinuousFunctions X) = 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
thus 0. (R_Normed_Algebra_of_ContinuousFunctions X) = X --> 0 by Th12
.= 0. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) by C0SP1:25 ; :: thesis: verum