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