let L be Field; :: thesis: for p being Polynomial of L
for x being Element of L
for n being 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 Nat holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)
let x be Element of L; :: thesis: for n being Nat holds eval ((p `^ n),x) = (power L) . ((eval (p,x)),n)
defpred S1[ Nat] means eval ((p `^ $1),x) = (power L) . ((eval (p,x)),$1);
A1: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
eval ((p `^ (n + 1)),x) = eval (((p `^ n) *' p),x) by Th19
.= ((power L) . ((eval (p,x)),n)) * (eval (p,x)) by A2, POLYNOM4:24
.= (power L) . ((eval (p,x)),(n + 1)) by GROUP_1:def 7 ;
hence S1[n + 1] ; :: thesis: verum
end;
eval ((p `^ 0),x) = eval ((1_. L),x) by Th15
.= 1_ L by POLYNOM4:18
.= (power L) . ((eval (p,x)),0) by GROUP_1:def 7 ;
then A3: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A3, A1); :: thesis: verum