:: deftheorem Def21 defines the_left_operation_of GROUP_10:def 21 :
for G being finite Group
for p being prime Nat
for H being Subgroup of G
for b₄ being LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)) holds
( b₄ = the_left_operation_of (H,p) iff for h being Element of H holds b₄ . h = the_left_translation_of (h,p) );