theorem Th25: :: AUTGROUP:25

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