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

per cases ( ( i >= 0 & j >= 0 ) or ( i >= 0 & j < 0 ) or ( i < 0 & j >= 0 ) or ( j < 0 & i < 0 ) ) ;

suppose ( i >= 0 & j >= 0 ) ; :: thesis: h |^ (i * j) = (h |^ i) |^ j

then reconsider m = i, n = j as Element of NAT by INT_1:3;
thus h |^ (i * j) = (h |^ m) |^ n by Lm7
.= (h |^ i) |^ j ; :: thesis: verum

end;

suppose ( i >= 0 & j < 0 ) ; :: thesis: h |^ (i * j) = (h |^ i) |^ j

then reconsider m = i, n = - j as Element of NAT by INT_1:3;
i * j = - (i * n) ;
hence h |^ (i * j) = (h |^ (i * n)) " by Lm12
.= (h ") |^ (i * n) by Lm17
.= ((h ") |^ m) |^ n by Lm7
.= ((h |^ i) ") |^ n by Lm17
.= (((h |^ i) ") |^ j) " by Lm12
.= (((h |^ i) |^ j) ") " by Lm17
.= (h |^ i) |^ j ;
:: thesis: verum

end;

suppose ( i < 0 & j >= 0 ) ; :: thesis: h |^ (i * j) = (h |^ i) |^ j

then reconsider m = - i, n = j as Element of NAT by INT_1:3;
i * j = - (m * j) ;
hence h |^ (i * j) = (h |^ (m * j)) " by Lm12
.= (h ") |^ (m * j) by Lm17
.= ((h ") |^ m) |^ n by Lm7
.= (((h ") |^ i) ") |^ n by Lm12
.= (((h |^ i) ") ") |^ j by Lm17
.= (h |^ i) |^ j ;
:: thesis: verum

end;

suppose ( j < 0 & i < 0 ) ; :: thesis: h |^ (i * j) = (h |^ i) |^ j

then reconsider m = - i, n = - j as Element of NAT by INT_1:3;
(i * j) * ((- 1) * (- 1)) = m * n ;
hence h |^ (i * j) = (h |^ m) |^ n by Lm7
.= ((h |^ (- i)) |^ j) " by Lm12
.= (((h |^ i) ") |^ j) " by Lm12
.= (((h ") |^ i) |^ j) " by Lm17
.= (((h ") |^ i) ") |^ j by Lm17
.= (((h ") ") |^ i) |^ j by Lm17
.= (h |^ i) |^ j ;
:: thesis: verum

end;

end;