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 holds
( Support (HM p,O) = {} or Support (HM p,O) = {(HT p,O)} )
let O be connected TermOrder of n; :: thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds
( Support (HM p,O) = {} or Support (HM p,O) = {(HT p,O)} )
let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of n,L holds
( Support (HM p,O) = {} or Support (HM p,O) = {(HT p,O)} )
let p be Polynomial of n,L; :: thesis: ( Support (HM p,O) = {} or Support (HM p,O) = {(HT p,O)} )
assume A1: not Support (HM p,O) = {} ; :: thesis: Support (HM p,O) = {(HT p,O)}
then A2: ex b being bag of n st Support (HM p,O) = {b} by POLYNOM7:6;

now

per cases ( HC p,O = 0. L or HC p,O <> 0. L ) ;

case HC p,O = 0. L ; :: thesis: Support (HM p,O) = {(HT p,O)}

hence Support (HM p,O) = {(HT p,O)} by A1, Lm10; :: thesis: verum

end;

case HC p,O <> 0. L ; :: thesis: Support (HM p,O) = {(HT p,O)}

then HT p,O in Support (HM p,O) by Lm9;
hence Support (HM p,O) = {(HT p,O)} by A2, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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