theorem Th21: :: AUTGROUP:21

for G being Group
for a, b being Element of G holds Conjugate (a * b) = (Conjugate b) * (Conjugate a)