theorem :: GROUP_5:29

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