let T1, T2 be LeftOperation of H,(the_sylow_p-subgroups_of_prime (p,G)); :: thesis: ( ( for h being Element of H holds T1 . h = the_left_translation_of (h,p) ) & ( for h being Element of H holds T2 . h = the_left_translation_of (h,p) ) implies T1 = T2 )
assume that
A26: for h being Element of H holds T1 . h = the_left_translation_of (h,p) and
A27: for h being Element of H holds T2 . h = the_left_translation_of (h,p) ; :: thesis: T1 = T2
let x be Element of H; :: according to FUNCT_2:def 8 :: thesis: ^ = ^
thus T1 . x = the_left_translation_of (x,p) by A26
.= T2 . x by A27 ; :: thesis: verum