let X be non empty compact TopSpace; :: thesis: 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X)
thus 1. (R_Normed_Algebra_of_ContinuousFunctions X) = 1_ (R_Algebra_of_ContinuousFunctions X)
.= X --> 1 by Th7
.= 1_ (R_Algebra_of_BoundedFunctions the carrier of X) by C0SP1:16
.= 1. (R_Normed_Algebra_of_BoundedFunctions the carrier of X) ; :: thesis: verum