set X = the ComplexNormSpace;
take C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace ; :: thesis:
thus ( C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is reflexive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is discerning & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is ComplexNormSpace-like & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is Abelian & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is add-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_zeroed & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_complementable & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right_unital & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is right-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is vector-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-distributive & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is vector-associative & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is scalar-unital & C_Normed_Algebra_of_BoundedLinearOperators the ComplexNormSpace is strict ) by Th20; :: thesis: