:: deftheorem defines R_Normed_Space_of_C_0_Functions C0SP3:def 13 :
for X being non empty TopSpace
for T being NormedLinearTopSpace holds R_Normed_Space_of_C_0_Functions (X,T) = NORMSTR(# (C_0_Functions (X,T)),(Zero_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Add_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(Mult_ ((C_0_Functions (X,T)),(RealVectSpace ( the carrier of X,T)))),(C_0_FunctionsNorm (X,T)) #);