theorem Th79: :: GROUP_1A:278

for G being addGroup
for a being Element of G holds a * (carr ((Omega). G)) = { b where b is Element of G : a,b are_conjugated }