theorem :: GROUP_5:18

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