let S be 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)
let T be NormedLinearTopSpace; R_VectorSpace_of_ContinuousFunctions (S,T) is Subspace of R_VectorSpace_of_BoundedFunctions ( the carrier of S,T)
A1:
the carrier of (R_VectorSpace_of_ContinuousFunctions (S,T)) c= the carrier of (R_VectorSpace_of_BoundedFunctions ( the carrier of S,T))
by Th34;
A2:
R_VectorSpace_of_ContinuousFunctions (S,T) is Subspace of RealVectSpace ( the carrier of S,T)
by Th5, RSSPACE:11;
R_VectorSpace_of_BoundedFunctions ( the carrier of S,T) is Subspace of RealVectSpace ( the carrier of S,T)
by RSSPACE4:7;
hence
R_VectorSpace_of_ContinuousFunctions (S,T) is Subspace of R_VectorSpace_of_BoundedFunctions ( the carrier of S,T)
by A1, A2, RLSUB_1:28; verum