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)) . b1 = (0_. R) . b1
per cases ( i = n or i <> n ) ;
suppose A2: i = n ; :: thesis: (anpoly (a,n)) . b1 = (0_. R) . b1
(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)) . b1 = (0_. R) . b1
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