for X being non empty TopSpace holds R_VectorSpace_of_C_0_Functions X is Subspace of RealVectSpace the carrier of X by RSSPACE:11;