let f be Element of the carrier of (Polynom-Ring INT.Ring); :: thesis: for n being Nat holds ^ (f |^ n) = (^ f) |^ n
let n be Nat; :: thesis: ^ (f |^ n) = (^ f) |^ n
set PRI = Polynom-Ring INT.Ring;
set PRF = Polynom-Ring F_Real;
defpred S₁[ Nat] means ^ (f |^ $1) = (^ f) |^ $1;
A1: S₁[ 0 ]

proof

A2: Polynom-Ring INT.Ring is Subring of Polynom-Ring F_Real by FIELD_4:def 1;
A3: f |^ 0 = 1_ (Polynom-Ring INT.Ring) by BINOM:8
.= 1. (Polynom-Ring INT.Ring) ;
(^ f) |^ 0 = 1_ (Polynom-Ring F_Real) by BINOM:8
.= 1. (Polynom-Ring F_Real) ;
hence S₁[ 0 ] by A3, A2, C0SP1:def 3; :: thesis: verum

end;

A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
f |^ (k + 1) = (f |^ k) * (f |^ 1) by BINOM:10
.= (f |^ k) * f by BINOM:8 ;
then ^ (f |^ (k + 1)) = ((^ f) |^ k) * (^ f) by A5, E_TRANS1:27
.= ((^ f) |^ k) * ((^ f) |^ 1) by BINOM:8
.= (^ f) |^ (k + 1) by BINOM:10 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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