:: deftheorem defines R_VectorSpace_of_ContinuousFunctions C0SP3:def 4 :
for S, T being RealNormSpace holds R_VectorSpace_of_ContinuousFunctions (S,T) = RLSStruct(# (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)))) #);