for S being non empty compact TopSpace
for T being NormedLinearTopSpace holds R_VectorSpace_of_ContinuousFunctions (S,T) is Subspace of R_VectorSpace_of_BoundedFunctions ( the carrier of S,T)