theorem :: GROUP_5:26

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