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