theorem :: GRNILP_1:1

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