:: deftheorem defines C_Normed_Space_of_C_0_Functions CC0SP2:def 10 :
for X being non empty TopSpace holds C_Normed_Space_of_C_0_Functions X = CNORMSTR(# (CC_0_Functions X),(Zero_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Add_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(Mult_ ((CC_0_Functions X),(ComplexVectSpace the carrier of X))),(CC_0_FunctionsNorm X) #);