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