theorem Th43: :: LOPBAN_9:25

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