theorem Th5: :: GRNILP_1:5

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