theorem Th4: :: GRNILP_1:4

for G being Group
for a, b being Element of G holds ([.a,(b ").] |^ b) " = [.(b "),a.] |^ b