theorem Th7: :: GRNILP_1:7

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