theorem :: GROUP_5:31

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