:: deftheorem defines CContinuousFunctionsNorm CC0SP2:def 5 :
for X being non empty compact TopSpace holds CContinuousFunctionsNorm X = (ComplexBoundedFunctionsNorm the carrier of X) | (CContinuousFunctions X);