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 >= 0 or j < - 1 or j = - 1 ) by Lm15;

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

then reconsider n = j as Element of NAT by INT_1:16;
A3: n + 1 >= 0 ;
A4: n + 1 = abs (j + 1) by ABSVALUE:def 1;
thus (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = (h |^ (abs (j + 1))) * ((h |^ (- 1)) * (h |^ (- j))) by A3, Def9
.= (h |^ (abs (j + 1))) * ((h " ) * (h |^ (- j))) by Th62
.= (h |^ (abs (j + 1))) * ((h " ) * ((h |^ j) " )) by Lm12
.= (h |^ (abs (j + 1))) * ((h " ) * ((h |^ (abs j)) " )) by A2, Def9
.= (h |^ (abs (j + 1))) * (((h |^ (abs j)) * h) " ) by Th25
.= (h |^ (abs (j + 1))) * ((h |^ ((abs j) + 1)) " ) by Lm6
.= (h |^ (abs (j + 1))) * ((h |^ (abs (j + 1))) " ) by A4, ABSVALUE:def 1
.= 1_ G by Def6 ; :: thesis: verum

end;

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

then A5: j + 1 < (- 1) + 1 by XREAL_1:8;
hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = ((h |^ (abs (j + 1))) " ) * ((h |^ (- 1)) * (h |^ (- j))) by Def9
.= ((h |^ (abs (j + 1))) " ) * ((h " ) * (h |^ (- j))) by Th62
.= (((h |^ (abs (j + 1))) " ) * (h " )) * (h |^ (- j)) by Def4
.= ((h * (h |^ (abs (j + 1)))) " ) * (h |^ (- j)) by Th25
.= ((h |^ ((abs (j + 1)) + 1)) " ) * (h |^ (- j)) by Lm6
.= ((h |^ ((- (j + 1)) + 1)) " ) * (h |^ (- j)) by A5, ABSVALUE:def 1
.= 1_ G by Def6 ;
:: thesis: verum

end;

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

hence (h |^ (j + 1)) * ((h |^ (- 1)) * (h |^ (- j))) = (1_ G) * ((h |^ (- 1)) * (h |^ (- j))) by Lm3
.= (h |^ (- 1)) * (h |^ (- j)) by Def5
.= (h " ) * (h |^ (- j)) by Th62
.= (h " ) * ((h |^ j) " ) by Lm12
.= (h " ) * ((h " ) " ) by A6, Th62
.= 1_ G by Def6 ;
:: thesis: verum

end;

end;

end;

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