for G being Group
for g, h being Element of G holds
( g * h = h * g iff g * (h ") = (h ") * g )