:: deftheorem Def6 defines Conjugate AUTGROUP:def 6 :
for G being Group
for b being Element of G
for b₃ being Element of InnAut G holds
( b₃ = Conjugate b iff for a being Element of G holds b₃ . a = a |^ b );