for X, Y being RealNormSpace
for Z being RealBanachSpace holds R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealBanachSpace