for p being Polynomial of R st ( for a being Element of NAT holds p . a = 0. R ) holds

p = 0_. R

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

p = 0_. R

proof

then consider a being Element of NAT such that
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

end;assume AS: for a being Element of NAT holds p . a = 0. R ; :: thesis: p = 0_. R

now :: thesis: not len p <> 0

hence
p = 0_. R
by POLYNOM4:5; :: thesis: verumassume
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;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

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