let L be Field; :: thesis: for p being Polynomial of L
for x being Element of L
for n being Element of NAT holds eval (p `^ n),x = (power L) . (eval p,x),n
let p be Polynomial of L; :: thesis: for x being Element of L
for n being Element of NAT holds eval (p `^ n),x = (power L) . (eval p,x),n
let x be Element of L; :: thesis: for n being Element of NAT holds eval (p `^ n),x = (power L) . (eval p,x),n
defpred S<sub>1</sub>[ Element of NAT ] means eval (p `^ $1),x = (power L) . (eval p,x),$1;

A1: now

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
eval (p `^ (n + 1)),x = eval ((p `^ n) *' p),x by Th20
.= ((power L) . (eval p,x),n) * (eval p,x) by A2, POLYNOM4:27
.= (power L) . (eval p,x),(n + 1) by GROUP_1:def 8 ;
hence S₁[n + 1] ; :: thesis: verum

end;

eval (p `^ 0 ),x = eval (1_. L),x by Th16
.= 1_ L by POLYNOM4:21
.= (power L) . (eval p,x),0 by GROUP_1:def 8 ;
then A3: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A1); :: thesis: verum