:: deftheorem defines C_Normed_Algebra_of_BoundedLinearOperators CLOPBAN2:def 8 :
for X being ComplexNormSpace holds C_Normed_Algebra_of_BoundedLinearOperators X = Normed_Complex_AlgebraStr(# (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)))),(BoundedLinearOperatorsNorm (X,X)) #);