theorem :: AUTGROUP:24

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