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 Th22, RSSPACE3:2; :: thesis: verum