for A being commutative Group
for a, b being Element of A holds (a * b) " = (a ") * (b ") by Th16;