let i be Integer; :: thesis: for G being Group
for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
let G be Group; :: thesis: for a, b being Element of G holds [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
let a, b be Element of G; :: thesis: [.a,(b |^ i).] = ((b |^ a) |^ (- i)) * (b |^ i)
thus [.a,(b |^ i).] = ((b |^ (- i)) |^ a) * (b |^ i) by GROUP_1:36
.= ((b |^ a) |^ (- i)) * (b |^ i) by GROUP_3:28 ; :: thesis: verum