consider X being RealNormSpace;
take R_Normed_Algebra_of_BoundedLinearOperators X ; :: thesis:
thus ( R_Normed_Algebra_of_BoundedLinearOperators X is reflexive & R_Normed_Algebra_of_BoundedLinearOperators X is discerning & R_Normed_Algebra_of_BoundedLinearOperators X is RealNormSpace-like & R_Normed_Algebra_of_BoundedLinearOperators X is Abelian & R_Normed_Algebra_of_BoundedLinearOperators X is add-associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_zeroed & R_Normed_Algebra_of_BoundedLinearOperators X is right_complementable & R_Normed_Algebra_of_BoundedLinearOperators X is associative & R_Normed_Algebra_of_BoundedLinearOperators X is right_unital & R_Normed_Algebra_of_BoundedLinearOperators X is right-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-associative & R_Normed_Algebra_of_BoundedLinearOperators X is vector-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-distributive & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-associative & R_Normed_Algebra_of_BoundedLinearOperators X is scalar-unital & R_Normed_Algebra_of_BoundedLinearOperators X is strict ) by Th20; :: thesis: