:: deftheorem defines R_NormSpace_of_ContinuousFunctions C0SP3:def 8 :
for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds R_NormSpace_of_ContinuousFunctions (S,T) = NORMSTR(# (ContinuousFunctions (S,T)),(Zero_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Add_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(Mult_ ((ContinuousFunctions (S,T)),(RealVectSpace ( the carrier of S,T)))),(ContinuousFunctionsNorm (S,T)) #);