:: deftheorem defines Banach_Algebra-like_3 CLOPBAN2:def 11 :
for X being non empty Normed_Complex_AlgebraStr holds
( X is Banach_Algebra-like_3 iff for a being Complex
for x, y being Element of X holds a * (x * y) = x * (a * y) );