let X be non empty compact TopSpace; :: thesis: 0. (C_Normed_Algebra_of_ContinuousFunctions X) = 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)
thus 0. (C_Normed_Algebra_of_ContinuousFunctions X) = X --> 0 by Th20
.= 0. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) by CC0SP1:18 ; :: thesis: verum