set X = the RealNormSpace;

take R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace ; :: thesis: ( 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 )

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: verum

take R_Normed_Algebra_of_BoundedLinearOperators the RealNormSpace ; :: thesis: ( 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 )

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: verum