theorem :: CLOPBAN2:16

for X being ComplexNormSpace holds C_Algebra_of_BoundedLinearOperators X is ComplexBLAlgebra ;