let n be Element of NAT ; :: thesis: for G, H being Group
for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
let G, H be Group; :: thesis: for a being Element of G
for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
let a be Element of G; :: thesis: for g being Homomorphism of G,H holds g . (a |^ n) = (g . a) |^ n
let g be Homomorphism of G,H; :: thesis: g . (a |^ n) = (g . a) |^ n
defpred S₁[ Element of NAT ] means g . (a |^ $1) = (g . a) |^ $1;
A1: S₁[ 0 ]

proof

thus g . (a |^ 0 ) = g . (1_ G) by GROUP_1:43
.= 1_ H by Th40
.= (g . a) |^ 0 by GROUP_1:43 ; :: thesis: verum

end;

A2: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
thus g . (a |^ (n + 1)) = g . ((a |^ n) * a) by GROUP_1:66
.= ((g . a) |^ n) * (g . a) by A3, Def7
.= (g . a) |^ (n + 1) by GROUP_1:66 ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A2);
hence g . (a |^ n) = (g . a) |^ n ; :: thesis: verum