theorem Th43: :: LOPBAN11:9

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