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

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

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

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

end;

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

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

end;

end;