:: deftheorem defines C_Algebra_of_BoundedLinearOperators CLOPBAN2:def 7 :
for X being ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators X = ComplexAlgebraStr(# (BoundedLinearOperators (X,X)),(FuncMult X),(Add_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))),(FuncUnit X),(Zero_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) #);