for X being non empty set
for Y being RealNormSpace holds R_NormSpace_of_BoundedFunctions (X,Y) is RealNormSpace