let G be Group; :: thesis: for g being Element of G
for i, j being Integer st g |^ i = g |^ j holds
g |^ (- i) = g |^ (- j)
let g be Element of G; :: thesis: for i, j being Integer st g |^ i = g |^ j holds
g |^ (- i) = g |^ (- j)
let i, j be Integer; :: thesis: ( g |^ i = g |^ j implies g |^ (- i) = g |^ (- j) )
assume A1: g |^ i = g |^ j ; :: thesis: g |^ (- i) = g |^ (- j)
thus g |^ (- j) = (g |^ (- j)) * (1_ G) by GROUP_1:def 4
.= (g |^ (- j)) * (g |^ 0) by GROUP_1:25
.= (g |^ (- j)) * (g |^ (i + (- i)))
.= (g |^ (- j)) * ((g |^ i) * (g |^ (- i))) by GROUP_1:33
.= ((g |^ (- j)) * (g |^ i)) * (g |^ (- i)) by GROUP_1:def 3
.= ((g |^ (- j)) * (g |^ j)) * (g |^ (- i)) by A1
.= (g |^ ((- j) + j)) * (g |^ (- i)) by GROUP_1:33
.= (1_ G) * (g |^ (- i)) by GROUP_1:25
.= g |^ (- i) by GROUP_1:def 4 ; :: thesis: verum