theorem Th39: :: LOPBAN10:51

for X being RealNormSpace-Sequence
for Y being RealNormSpace holds R_NormSpace_of_BoundedMultilinearOperators (X,Y) is RealNormSpace