:: deftheorem Def2 defines the_left_operation_of GROUP_10:def 2 :
for S being non empty Group-like associative multMagma
for b₂ being LeftOperation of S, the carrier of S holds
( b₂ = the_left_operation_of S iff for s being Element of S holds b₂ . s = the_left_translation_of s );