theorem :: GROUP_5:21

for G being Group
for a being Element of G holds
( [.a,(a ").] = 1_ G & [.(a "),a.] = 1_ G )