set q = anpoly (a,n);
A1: a = 0. R by STRUCT_0:def 12;

now :: thesis: for i being Element of NAT holds (anpoly (a,n)) . i = (0_. R) . i

let i be Element of NAT ; :: thesis: (anpoly (a,n)) . b₁ = (0_. R) . b₁

per cases ( i = n or i <> n ) ;

suppose A2: i = n ; :: thesis: (anpoly (a,n)) . b₁ = (0_. R) . b₁

(anpoly (a,n)) . n = 0. R by A1, POLYDIFF:24
.= (0_. R) . n by FUNCOP_1:7, ORDINAL1:def 12 ;
hence (anpoly (a,n)) . i = (0_. R) . i by A2; :: thesis: verum

end;

suppose i <> n ; :: thesis: (anpoly (a,n)) . b₁ = (0_. R) . b₁

then (anpoly (a,n)) . i = 0. R by POLYDIFF:25
.= (0_. R) . i by FUNCOP_1:7 ;
hence (anpoly (a,n)) . i = (0_. R) . i ; :: thesis: verum

end;

end;

end;

then anpoly (a,n) = 0_. R ;
hence anpoly (a,n) is zero ; :: thesis: verum