:: deftheorem defines R_NormSpace_of_ContinuousFunctions ORDEQ_01:def 6 :
for X being non empty closed_interval Subset of REAL
for Y being RealNormSpace holds R_NormSpace_of_ContinuousFunctions (X,Y) = NORMSTR(# (ContinuousFunctions (X,Y)),(Zero_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Add_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(Mult_ ((ContinuousFunctions (X,Y)),(R_VectorSpace_of_BoundedFunctions (X,Y)))),(ContinuousFunctionsNorm (X,Y)) #);