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