take C_Normed_Algebra_of_BoundedLinearOperators the non trivial ComplexBanachSpace ; :: thesis: C_Normed_Algebra_of_BoundedLinearOperators the non trivial ComplexBanachSpace is Banach_Algebra-like
thus C_Normed_Algebra_of_BoundedLinearOperators the non trivial ComplexBanachSpace is Banach_Algebra-like ; :: thesis: verum