let n be Ordinal; :: thesis: for O being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC (p,O) = 0. L iff p = 0_ (n,L) )
let O be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for p being Polynomial of n,L holds
( HC (p,O) = 0. L iff p = 0_ (n,L) )
let L be non empty ZeroStr ; :: thesis: for p being Polynomial of n,L holds
( HC (p,O) = 0. L iff p = 0_ (n,L) )
let p be Polynomial of n,L; :: thesis: ( HC (p,O) = 0. L iff p = 0_ (n,L) )

now :: thesis: ( HC (p,O) = 0. L implies p = 0_ (n,L) )

assume HC (p,O) = 0. L ; :: thesis: p = 0_ (n,L)
then not HT (p,O) in Support p by POLYNOM1:def 4;
then Support p = {} by Def6;
hence p = 0_ (n,L) by POLYNOM7:1; :: thesis: verum

end;

hence ( HC (p,O) = 0. L iff p = 0_ (n,L) ) by POLYNOM1:22; :: thesis: verum