theorem Th38: :: CLOPBAN1:38

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