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 Th19
.= (a |^ (- i)) * ((a |^ i) |^ b) by GROUP_1:70
.= (a |^ (- i)) * ((a |^ b) |^ i) by GROUP_3:34 ; :: thesis: verum