:: deftheorem defines ContinuousFunctionsNorm C0SP2:def 4 :
for X being non empty compact TopSpace holds ContinuousFunctionsNorm X = (BoundedFunctionsNorm the carrier of X) | (ContinuousFunctions X);