:: deftheorem Def4 defines the_extension_of_left_translation_of GROUP_10:def 4 :
for E being non empty set
for n being Nat
for S being non empty Group-like multMagma
for s being Element of S
for LO being LeftOperation of S,E st card n c= card E holds
for b₆ being Function of (the_subsets_of_card (n,E)),(the_subsets_of_card (n,E)) holds
( b₆ = the_extension_of_left_translation_of (n,s,LO) iff for X being Element of the_subsets_of_card (n,E) holds b₆ . X = (LO ^ s) .: X );