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

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

suppose i >= 0 ; :: thesis: (h ") |^ i = (h |^ i) "

then reconsider n = i as Element of NAT by INT_1:3;
thus (h ") |^ i = (h |^ n) " by Lm8
.= (h |^ i) " ; :: thesis: verum

end;

suppose A1: i < 0 ; :: thesis: (h ") |^ i = (h |^ i) "

hence (h ") |^ i = ((h ") |^ |.i.|) " by Def8
.= ((h |^ |.i.|) ") " by Lm8
.= (h |^ i) " by A1, Def8 ;
:: thesis: verum

end;

end;