theorem Th18: :: GROUP_1:19

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