let X be non empty compact TopSpace; :: thesis: 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X)
thus 1. (C_Normed_Algebra_of_ContinuousFunctions X) = 1_ (C_Algebra_of_ContinuousFunctions X)
.= X --> 1r by Th14
.= 1_ (C_Algebra_of_BoundedFunctions the carrier of X) by CC0SP1:9
.= 1. (C_Normed_Algebra_of_BoundedFunctions the carrier of X) ; :: thesis: verum