let i be Integer; :: thesis: for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
let G, H be Group; :: thesis: for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
let a be Element of G; :: thesis: for g being Homomorphism of G,H holds g . (a |^ i) = (g . a) |^ i
let g be Homomorphism of G,H; :: thesis: g . (a |^ i) = (g . a) |^ i

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

suppose A1: i >= 0 ; :: thesis: g . (a |^ i) = (g . a) |^ i

hence g . (a |^ i) = g . (a |^ |.i.|) by ABSVALUE:def 1
.= (g . a) |^ |.i.| by Th36
.= (g . a) |^ i by A1, ABSVALUE:def 1 ;
:: thesis: verum

end;

suppose A2: i < 0 ; :: thesis: g . (a |^ i) = (g . a) |^ i

hence g . (a |^ i) = g . ((a |^ |.i.|) ") by GROUP_1:30
.= (g . (a |^ |.i.|)) " by Th32
.= ((g . a) |^ |.i.|) " by Th36
.= (g . a) |^ i by A2, GROUP_1:30 ;
:: thesis: verum

end;

end;