let S be non empty compact TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: verum