theorem Th39: :: LOPBAN_9:22

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