theorem :: AUTGROUP:27

for G being Group
for a being Element of G holds
( (Conjugate a) * (Conjugate (1_ G)) = Conjugate a & (Conjugate (1_ G)) * (Conjugate a) = Conjugate a )