:: deftheorem Def5 defines the_extension_of_left_operation_of GROUP_10:def 5 :
for E being non empty set
for n being Nat
for S being non empty Group-like multMagma
for LO being LeftOperation of S,E st card n c= card E holds
for b₅ being LeftOperation of S,(the_subsets_of_card (n,E)) holds
( b₅ = the_extension_of_left_operation_of (n,LO) iff for s being Element of S holds b₅ . s = the_extension_of_left_translation_of (n,s,LO) );