let i be Integer; :: thesis: for G being Group

for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)

let G be Group; :: thesis: for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)

let a, b be Element of G; :: thesis: [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)

thus [.(a |^ i),b.] = ((a |^ i) ") * (((b ") * (a |^ i)) * b) by Th16

.= (a |^ (- i)) * ((a |^ i) |^ b) by GROUP_1:36

.= (a |^ (- i)) * ((a |^ b) |^ i) by GROUP_3:28 ; :: thesis: verum

for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)

let G be Group; :: thesis: for a, b being Element of G holds [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)

let a, b be Element of G; :: thesis: [.(a |^ i),b.] = (a |^ (- i)) * ((a |^ b) |^ i)

thus [.(a |^ i),b.] = ((a |^ i) ") * (((b ") * (a |^ i)) * b) by Th16

.= (a |^ (- i)) * ((a |^ i) |^ b) by GROUP_1:36

.= (a |^ (- i)) * ((a |^ b) |^ i) by GROUP_3:28 ; :: thesis: verum