:: deftheorem defines R_VectorSpace_of_ContinuousFunctions C0SP3:def 2 :
for S being non empty TopSpace
for T being LinearTopSpace 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)))) #);