let i be Integer; :: thesis: for G being Group
for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
let G be Group; :: thesis: for g, h being Element of G st g * h = h * g holds
g * (h |^ i) = (h |^ i) * g
let g, h be Element of G; :: thesis: ( g * h = h * g implies g * (h |^ i) = (h |^ i) * g )
assume A1: g * h = h * g ; :: thesis: g * (h |^ i) = (h |^ i) * g
thus g * (h |^ i) = (g |^ 1) * (h |^ i) by Th25
.= (h |^ i) * (g |^ 1) by A1, Th38
.= (h |^ i) * g by Th25 ; :: thesis: verum