:: deftheorem defines Banach_Algebra-like_1 CLOPBAN2:def 9 :
for X being non empty Normed_Complex_AlgebraStr holds
( X is Banach_Algebra-like_1 iff for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.|| );