let X, Y be ComplexNormSpace; :: thesis: C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace
CLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(C_VectorSpace_of_LinearOperators (X,Y)))) #) is ComplexLinearSpace ;
hence C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace by Th37, CSSPACE3:2; :: thesis: verum