let n be Ordinal; :: thesis: for O being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L st HC p,O <> 0. L holds
HT p,O in Support (HM p,O)
let O be connected TermOrder of n; :: thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L st HC p,O <> 0. L holds
HT p,O in Support (HM p,O)
let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of n,L st HC p,O <> 0. L holds
HT p,O in Support (HM p,O)
let p be Polynomial of n,L; :: thesis: ( HC p,O <> 0. L implies HT p,O in Support (HM p,O) )
assume HC p,O <> 0. L ; :: thesis: HT p,O in Support (HM p,O)
then (HM p,O) . (HT p,O) <> 0. L by Lm8;
hence HT p,O in Support (HM p,O) by POLYNOM1:def 9; :: thesis: verum