let R be Ring; :: thesis: for p being Polynomial of R holds
( p = 0_. R iff { i where i is Nat : p . i <> 0. R } = {} )
let p be Polynomial of R; :: thesis: ( p = 0_. R iff { i where i is Nat : p . i <> 0. R } = {} )

hereby :: thesis: ( { i where i is Nat : p . i <> 0. R } = {} implies p = 0_. R )

assume AS: p = 0_. R ; :: thesis: { i where i is Nat : p . i <> 0. R } = {}

now :: thesis: { i where i is Nat : p . i <> 0. R } is empty

assume not { i where i is Nat : p . i <> 0. R } is empty ; :: thesis: contradiction
then consider x being object such that
H1: x in { i where i is Nat : p . i <> 0. R } ;
consider i being Nat such that
H2: ( x = i & p . i <> 0. R ) by H1;
thus contradiction by AS, H2, FUNCOP_1:7, ORDINAL1:def 12; :: thesis: verum

end;

hence { i where i is Nat : p . i <> 0. R } = {} ; :: thesis: verum

end;

assume AS: { i where i is Nat : p . i <> 0. R } = {} ; :: thesis: p = 0_. R
assume p <> 0_. R ; :: thesis: contradiction
then len p <> 0 by POLYNOM4:5;
then (len p) + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then reconsider k = (len p) - 1 as Element of NAT by INT_1:3;
reconsider k = k as Nat ;
len p = k + 1 ;
then p . k <> 0. R by ALGSEQ_1:10;
then k in { i where i is Nat : p . i <> 0. R } ;
hence contradiction by AS; :: thesis: verum