let j be Integer; :: thesis: for G being Group
for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
let G be Group; :: thesis: for h being Element of G holds h |^ (j - 1) = (h |^ j) * (h |^ (- 1))
let h be Element of G; :: thesis: h |^ (j - 1) = (h |^ j) * (h |^ (- 1))

A1: now

per cases ( j >= 1 or j < 0 or j = 0 ) by Lm13;

suppose A2: j >= 1 ; :: thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G

then j >= 1 + 0 ;
then A3: j - 1 >= 0 by XREAL_1:21;
then A4: (abs (j - 1)) + 1 = (j - 1) + 1 by ABSVALUE:def 1
.= j ;
A5: abs j = j by A2, ABSVALUE:def 1;
A6: abs j = abs (- j) by COMPLEX1:138;
thus (h |^ (j - 1)) * (h * (h |^ (- j))) = ((h |^ (j - 1)) * h) * (h |^ (- j)) by Def4
.= ((h |^ (abs (j - 1))) * h) * (h |^ (- j)) by A3, Def9
.= ((h |^ (abs (j - 1))) * h) * ((h |^ (abs (- j))) " ) by A2, Th60
.= (h |^ ((abs (j - 1)) + 1)) * ((h |^ (abs (- j))) " ) by Lm6
.= 1_ G by A4, A5, A6, Def6 ; :: thesis: verum

end;

suppose A7: j < 0 ; :: thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G

A8: 1 - j = - (j - 1) ;
thus (h |^ (j - 1)) * (h * (h |^ (- j))) = ((h |^ (abs (j - 1))) " ) * (h * (h |^ (- j))) by A7, Def9
.= ((h |^ (abs (j - 1))) " ) * (h * (h |^ (abs (- j)))) by A7, Def9
.= ((h |^ (abs (j - 1))) " ) * (h |^ (1 + (abs (- j)))) by Lm6
.= ((h |^ (abs (j - 1))) " ) * (h |^ (1 + (- j))) by A7, ABSVALUE:def 1
.= ((h |^ (abs (j - 1))) " ) * (h |^ (abs (j - 1))) by A7, A8, ABSVALUE:def 1
.= 1_ G by Def6 ; :: thesis: verum

end;

suppose A9: j = 0 ; :: thesis: (h |^ (j - 1)) * (h * (h |^ (- j))) = 1_ G

hence (h |^ (j - 1)) * (h * (h |^ (- j))) = (h " ) * (h * (h |^ (- j))) by Th62
.= ((h " ) * h) * (h |^ (- j)) by Def4
.= (1_ G) * (h |^ (- j)) by Def6
.= h |^ 0 by A9, Def5
.= 1_ G by Def8 ;
:: thesis: verum

end;

end;

end;

(h |^ (j - 1)) * (h |^ (1 - j)) = (h |^ (j - 1)) * (h |^ (- (j - 1)))
.= (h |^ (j - 1)) * ((h |^ (j - 1)) " ) by Lm12
.= 1_ G by Def6 ;
then h * (h |^ (- j)) = h |^ (1 - j) by A1, Th14;
then (h |^ (1 - j)) " = ((h |^ (- j)) " ) * (h " ) by Th25
.= (h |^ (- (- j))) * (h " ) by Lm12
.= (h |^ j) * (h |^ (- 1)) by Th62 ;
then (h |^ j) * (h |^ (- 1)) = h |^ (- (1 - j)) by Lm12;
hence h |^ (j - 1) = (h |^ j) * (h |^ (- 1)) ; :: thesis: verum