let X be non empty set ; :: thesis: for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions X,Y is RealNormSpace
let Y be RealNormSpace; :: thesis: R_NormSpace_of_BoundedFunctions X,Y is RealNormSpace
RLSStruct(# (BoundedFunctions X,Y),(Zero_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Add_ (BoundedFunctions X,Y),(RealVectSpace X,Y)),(Mult_ (BoundedFunctions X,Y),(RealVectSpace X,Y)) #) is RealLinearSpace ;
hence R_NormSpace_of_BoundedFunctions X,Y is RealNormSpace by Th25, RSSPACE3:4; :: thesis: verum