let R be domRing; :: thesis: 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 ; :: thesis: ( n <> 0 implies for a being Element of R holds eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n )
assume A: n <> 0 ; :: thesis: for a being Element of R holds eval ((<%(0. R),(1. R)%> `^ n),a) = a |^ n
let a be Element of R; :: thesis: 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 ;
:: thesis: verum