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