let i be Integer; :: thesis: for G being Group
for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
let G be Group; :: thesis: for h being Element of G st i <= 0 holds
h |^ i = (h |^ (abs i)) "
let h be Element of G; :: thesis: ( i <= 0 implies h |^ i = (h |^ (abs i)) " )
assume A1: i <= 0 ; :: thesis: h |^ i = (h |^ (abs i)) "

per cases ( i < 0 or i = 0 ) by A1;

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

hence h |^ i = (h |^ (abs i)) " by Def9; :: thesis: verum

end;

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

hence h |^ i = 1_ G by Lm3
.= (1_ G) " by Th16
.= (h |^ 0) " by Def8
.= (h |^ (abs i)) " by A2, ABSVALUE:def 1 ;
:: thesis: verum

end;

end;