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:16;
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 " ) |^ (abs i)) " by Def9
.= ((h |^ (abs i)) " ) " by Lm8
.= (h |^ i) " by A1, Def9 ;
:: thesis: verum

end;

end;