consider X being ComplexNormSpace;
take C_Normed_Algebra_of_BoundedLinearOperators X ; :: thesis:
thus ( 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 scalar-unital & C_Normed_Algebra_of_BoundedLinearOperators X is strict ) by Th20; :: thesis: