let R be domRing; for n being Element of NAT st n <> 0 holds
for a being Element of R holds eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
let n be Element of NAT ; ( n <> 0 implies for a being Element of R holds eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n )
assume A:
n <> 0
; for a being Element of R holds eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
let a be Element of R; eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
<%(0. R),(1. R)%> `^ n = anpoly ((1. R),n)
by FIELD_1:12;
hence eval ((<%(0. R),(1. R)%> `^ n),a) =
(1. R) * (a |^ n)
by A, FIELD_1:6
.=
a |^ n
;
verum