theorem Th39: :: LOPBAN_1:39

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