theorem Th79: :: GROUP_3:79

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