:: deftheorem defines are_conjugated_under GROUP_10:def 14 :
for S being non empty unital multMagma
for E being set
for T being LeftOperation of S,E
for x, y being Element of E holds
( x,y are_conjugated_under T iff ex s being Element of S st y = (T ^ s) . x );