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 Th42, CSSPACE3:4; :: thesis: verum