theorem :: C0SP3:59
for X being non empty TopSpace
for T being NormedLinearTopSpace holds R_VectorSpace_of_C_0_Functions (X,T) is Subspace of RealVectSpace ( the carrier of X,T) by RSSPACE:11;