theorem :: GROUP_5:24

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