theorem :: GROUP_5:42

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