consider X being non trivial RealBanachSpace;
take R_Normed_Algebra_of_BoundedLinearOperators X ; :: thesis: R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like
thus R_Normed_Algebra_of_BoundedLinearOperators X is Banach_Algebra-like ; :: thesis: verum