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

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