let k be Nat; :: thesis: for O being Ordinal
for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of O,R
for f being Function of O,R holds eval ((p `^ k),f) = (power R) . ((eval (p,f)),k)
let O be Ordinal; :: thesis: for R being non trivial right_complementable associative commutative Abelian add-associative right_zeroed right_unital well-unital distributive doubleLoopStr
for p being Polynomial of O,R
for f being Function of O,R holds eval ((p `^ k),f) = (power R) . ((eval (p,f)),k)
let R be non trivial right_complementable associative commutative Abelian add-associative right_zeroed right_unital well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of O,R
for f being Function of O,R holds eval ((p `^ k),f) = (power R) . ((eval (p,f)),k)
let p be Polynomial of O,R; :: thesis: for f being Function of O,R holds eval ((p `^ k),f) = (power R) . ((eval (p,f)),k)
let f be Function of O,R; :: thesis: eval ((p `^ k),f) = (power R) . ((eval (p,f)),k)
defpred S<sub>1</sub>[ Nat] means eval ((p `^ $1),f) = (power R) . ((eval (p,f)),$1);
eval ((p `^ 0),f) = eval ((1_ (O,R)),f) by Th28
.= 1_ R by POLYNOM2:21
.= (power R) . ((eval (p,f)),0) by GROUP_1:def 7 ;
then A1: S₁[ 0 ] ;
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]
thus eval ((p `^ (n + 1)),f) = eval (((p `^ n) *' p),f) by Th29
.= ((power R) . ((eval (p,f)),n)) * (eval (p,f)) by A3, POLYNOM2:25
.= (power R) . ((eval (p,f)),(n + 1)) by GROUP_1:def 7 ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence eval ((p `^ k),f) = (power R) . ((eval (p,f)),k) ; :: thesis: verum