theorem Th42: :: CLOPBAN1:42

for X being ComplexNormSpace
for Y being ComplexBanachSpace holds C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexBanachSpace