:: deftheorem Def8 defines the_left_translation_of GROUP_10:def 8 :
for G being Group
for H, P being Subgroup of G
for h being Element of H
for b₅ being Function of (Left_Cosets P),(Left_Cosets P) holds
( b₅ = the_left_translation_of (h,P) iff for P1 being Element of Left_Cosets P ex P2 being Element of Left_Cosets P ex A1, A2 being Subset of G ex g being Element of G st
( P2 = b₅ . P1 & A2 = g * A1 & A1 = P1 & A2 = P2 & g = h ) );