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
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
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
Support (HM p,O) = {}
let p be Polynomial of n,L; :: thesis: ( HC p,O = 0. L implies Support (HM p,O) = {} )
assume A1: HC p,O = 0. L ; :: thesis: Support (HM p,O) = {}
then p = 0_ n,L by Lm7;
then Support p = {} by POLYNOM7:1;
then A2: HT p,O = EmptyBag n by Def6;
A3: term (HM p,O) = EmptyBag n by A1, POLYNOM7:8;

now

assume Support (HM p,O) <> {} ; :: thesis: contradiction
then Support (HM p,O) = {(term (HM p,O))} by POLYNOM7:7;
then term (HM p,O) in Support (HM p,O) by TARSKI:def 1;
then (HM p,O) . (EmptyBag n) <> 0. L by A3, POLYNOM1:def 9;
hence contradiction by A1, A2, Lm8; :: thesis: verum

end;

hence Support (HM p,O) = {} ; :: thesis: verum