let R be domRing; :: thesis: for n being Element of NAT holds (<%(0. R),(1. R)%> `^ n) . n = 1. R
let n be Element of NAT ; :: thesis: (<%(0. R),(1. R)%> `^ n) . n = 1. R
<%(0. R),(1. R)%> `^ n = anpoly ((1. R),n) by FIELD_1:12;
hence (<%(0. R),(1. R)%> `^ n) . n = 1. R by POLYDIFF:24; :: thesis: verum