:: deftheorem Def9 defines the_left_operation_of GROUP_10:def 9 :
for G being Group
for H, P being Subgroup of G
for b₄ being LeftOperation of H,(Left_Cosets P) holds
( b₄ = the_left_operation_of (H,P) iff for h being Element of H holds b₄ . h = the_left_translation_of (h,P) );