theorem :: GROUP_5:43

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