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