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