let L be non empty non degenerated right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr ; :: 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 S<sub>1</sub>[ Nat] means eval ((p `^ $1),x) = (power L) . ((eval (p,x)),$1);

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be 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 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 S₁[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: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1); :: thesis: verum