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