let R be Ring; :: thesis: for S being R -homomorphic Ring
for f being unity-preserving multiplicative Function of R,S
for a being Element of R
for n being Nat holds f . (a |^ n) = (f . a) |^ n
let S be R -homomorphic Ring; :: thesis: for f being unity-preserving multiplicative Function of R,S
for a being Element of R
for n being Nat holds f . (a |^ n) = (f . a) |^ n
let f be unity-preserving multiplicative Function of R,S; :: thesis: for a being Element of R
for n being Nat holds f . (a |^ n) = (f . a) |^ n
let a be Element of R; :: thesis: for n being Nat holds f . (a |^ n) = (f . a) |^ n
let n be Nat; :: thesis: f . (a |^ n) = (f . a) |^ n
defpred S₁[ Nat] means f . (a |^ $1) = (f . a) |^ $1;
f . (a |^ 0) = f . (1_ R) by BINOM:8
.= 1_ S by GROUP_1:def 13
.= (f . a) |^ 0 by BINOM:8 ;
then IA: S₁[ 0 ] ;

IS: 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 IV: S₁[k] ; :: thesis: S₁[k + 1]
f . (a |^ (k + 1)) = f . ((a |^ k) * (a |^ 1)) by BINOM:10
.= (f . (a |^ k)) * (f . (a |^ 1)) by GROUP_6:def 6
.= ((f . a) |^ k) * (f . a) by IV, BINOM:8
.= ((f . a) |^ k) * ((f . a) |^ 1) by BINOM:8
.= (f . a) |^ (k + 1) by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence f . (a |^ n) = (f . a) |^ n ; :: thesis: verum