theorem Th28: :: GROUP_5:28
for G being Group
for a, b being Element of G holds [.a,(b ").] = [.b,a.] |^ (b ")