theorem :: GRNILP_1:3

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