:: deftheorem defines C_Normed_Algebra_of_ContinuousFunctions CC0SP2:def 6 :
for X being non empty compact TopSpace holds C_Normed_Algebra_of_ContinuousFunctions X = Normed_Complex_AlgebraStr(# (CContinuousFunctions X),(mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Add_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Mult_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(One_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(Zero_ ((CContinuousFunctions X),(CAlgebra the carrier of X))),(CContinuousFunctionsNorm X) #);