:: deftheorem defines ContinuousFunctionsNorm ORDEQ_01:def 4 :
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds ContinuousFunctionsNorm (X,Y) = (BoundedFunctionsNorm (X,Y)) | (ContinuousFunctions (X,Y));