for p being Polynomial of R st ( for a being Element of NAT holds p . a = 0. R ) holds
p = 0_. R
proof
let p be Polynomial of R; :: thesis: ( ( for a being Element of NAT holds p . a = 0. R ) implies p = 0_. R )
assume AS: for a being Element of NAT holds p . a = 0. R ; :: thesis: p = 0_. R
now :: thesis: not len p <> 0
assume len p <> 0 ; :: thesis: contradiction
then consider k being Nat such that
D3: len p = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
p . k <> 0. R by D3, ALGSEQ_1:10;
hence contradiction by AS; :: thesis: verum
end;
hence p = 0_. R by POLYNOM4:5; :: thesis: verum
end;
then consider a being Element of NAT such that
A: p . a <> 0. R ;
b * (p . a) <> 0. R by A, VECTSP_2:def 1;
then (b * p) . a <> 0. R by POLYNOM5:def 4;
hence not b * p is zero by FUNCOP_1:7; :: thesis: verum