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 4; :: thesis: verum