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 A1: i >= 0 ; :: thesis: h |^ (- i) = (h |^ i) "

per cases ( - i < - 0 or i = 0 ) by A1, XREAL_1:24;

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

hence h |^ (- i) = (h |^ |.(- i).|) " by Def8
.= (h |^ (- (- i))) " by A2, ABSVALUE:def 1
.= (h |^ i) " ;
:: thesis: verum

end;

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

hence h |^ (- i) = 1_ G by Lm3
.= (1_ G) " by Th8
.= (h |^ i) " by A3, Lm3 ;
:: thesis: verum

end;

end;

end;

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

then h |^ i = (h |^ |.i.|) " by Def8;
hence h |^ (- i) = (h |^ i) " by A4, ABSVALUE:def 1; :: thesis: verum

end;

end;