let n be Ordinal; 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; 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 ; 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; ( HC (p,O) = 0. L iff p = 0_ (n,L) )
hence
( HC (p,O) = 0. L iff p = 0_ (n,L) )
by POLYNOM1:22; verum