for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace