let R be domRing; :: thesis: for x being Element of (Polynom-Ring R)
for f being Polynomial of R st x = f holds
for n being Nat holds x |^ n = f `^ n
let x be Element of (Polynom-Ring R); :: thesis: for f being Polynomial of R st x = f holds
for n being Nat holds x |^ n = f `^ n
let f be Polynomial of R; :: thesis: ( x = f implies for n being Nat holds x |^ n = f `^ n )
assume A1: x = f ; :: thesis: for n being Nat holds x |^ n = f `^ n
defpred S₁[ Nat] means x |^ $1 = f `^ $1;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
x |^ (n + 1) = (x |^ n) * (x |^ 1) by BINOM:10
.= (x |^ n) * x by BINOM:8
.= (f `^ n) *' f by A1, A3, POLYNOM3:def 10
.= f `^ (n + 1) by POLYNOM5:19 ;
hence S₁[n + 1] ; :: thesis: verum

end;

x |^ 0 = 1_ (Polynom-Ring R) by BINOM:8
.= 1_. R by POLYNOM3:37
.= f `^ 0 by POLYNOM5:15 ;
then A4: S<sub>1</sub>[ 0 ] ;
for n being Nat holds S<sub>1</sub>[n] from NAT_1:sch 2(A4, A2);
hence for n being Nat holds x |^ n = f `^ n ; :: thesis: verum