:: deftheorem Def6 defines the_left_translation_of GROUP_10:def 6 :
for S being non empty multMagma
for s being Element of S
for Z being non empty set
for b₄ being Function of [: the carrier of S,Z:],[: the carrier of S,Z:] holds
( b₄ = the_left_translation_of (s,Z) iff for z1 being Element of [: the carrier of S,Z:] ex z2 being Element of [: the carrier of S,Z:] ex s1, s2 being Element of S ex z being Element of Z st
( z2 = b₄ . z1 & s2 = s * s1 & z1 = [s1,z] & z2 = [s2,z] ) );