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 Th6;
hence X --> 0 = 0. (R_Normed_Algebra_of_ContinuousFunctions X) ; :: thesis: verum