theorem :: C0SP3:15

for S, T being RealNormSpace holds R_VectorSpace_of_ContinuousFunctions (S,T) is Subspace of RealVectSpace ( the carrier of S,T) by Th11, RSSPACE:11;