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 :: thesis: not Support (HM (p,O)) <> {}

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 4;
hence contradiction by A1, A2, Lm8; :: thesis: verum

end;

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