theorem Th20: :: LOPBAN_2:20

for X being RealNormSpace holds
( 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 )