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