theorem Th17: :: TOPGRP_1:18

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