let X be non empty compact TopSpace; :: thesis: X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X)
X --> 0 = 0. (R_Algebra_of_ContinuousFunctions X) by ThB12Zero;
hence X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ; :: thesis: verum