:: deftheorem Def7 defines the_left_operation_of GROUP_10:def 7 :
for S being non empty Group-like associative multMagma
for Z being non empty set
for b₃ being LeftOperation of S,[: the carrier of S,Z:] holds
( b₃ = the_left_operation_of (S,Z) iff for s being Element of S holds b₃ . s = the_left_translation_of (s,Z) );