:: deftheorem defines C_VectorSpace_of_BoundedLinearOperators CLOPBAN1:def 8 :
for X, Y being ComplexNormSpace holds C_VectorSpace_of_BoundedLinearOperators (X,Y) = 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)))) #);