for X being ComplexNormSpace holds
( C_Normed_Algebra_of_BoundedLinearOperators X is reflexive & C_Normed_Algebra_of_BoundedLinearOperators X is discerning & C_Normed_Algebra_of_BoundedLinearOperators X is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators X is Abelian & C_Normed_Algebra_of_BoundedLinearOperators X is add-associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators X is associative & C_Normed_Algebra_of_BoundedLinearOperators X is right_unital & C_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital )