let R be Ring; :: thesis: for S being R -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R
for n being Nat holds h . (a |^ n) = (h . a) |^ n
let S be R -homomorphic Ring; :: thesis: for h being Homomorphism of R,S
for a being Element of R
for n being Nat holds h . (a |^ n) = (h . a) |^ n
let h be Homomorphism of R,S; :: thesis: for a being Element of R
for n being Nat holds h . (a |^ n) = (h . a) |^ n
let a be Element of R; :: thesis: for n being Nat holds h . (a |^ n) = (h . a) |^ n
let n be Nat; :: thesis: h . (a |^ n) = (h . a) |^ n
defpred S₁[ Nat] means h . (a |^ $1) = (h . a) |^ $1;
A1: S₁[ 0 ]

proof

thus h . (a |^ 0) = h . (1_ R) by BINOM:8
.= 1_ S by GROUP_1:def 13
.= (h . a) |^ 0 by BINOM:8 ; :: thesis: verum

end;

A2: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
h . (a |^ (k + 1)) = h . ((a |^ k) * (a |^ 1)) by BINOM:10
.= (h . (a |^ k)) * (h . (a |^ 1)) by GROUP_6:def 6
.= ((h . a) |^ k) * (h . a) by A3, BINOM:8
.= ((h . a) |^ k) * ((h . a) |^ 1) by BINOM:8
.= (h . a) |^ (k + 1) by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence h . (a |^ n) = (h . a) |^ n ; :: thesis: verum