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