theorem Th16: :: GROUP_1:17

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