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 }