for G being Group
for a being Element of G holds (a *) /" = (a ") *