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 |^ (abs i)) by ABSVALUE:def 1
.= (g . a) |^ (abs i) by Th45
.= (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 |^ (abs i)) " ) by GROUP_1:60
.= (g . (a |^ (abs i))) " by Th41
.= ((g . a) |^ (abs i)) " by Th45
.= (g . a) |^ i by A2, GROUP_1:60 ;
:: thesis: verum

end;

end;