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