let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L
for b being bag of n st b <> HT p,T holds
(HM p,T) . b = 0. L
let O be connected TermOrder of n; :: thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L
for b being bag of n st b <> HT p,O holds
(HM p,O) . b = 0. L
let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of n,L
for b being bag of n st b <> HT p,O holds
(HM p,O) . b = 0. L
let p be Polynomial of n,L; :: thesis: for b being bag of n st b <> HT p,O holds
(HM p,O) . b = 0. L
let b be bag of n; :: thesis: ( b <> HT p,O implies (HM p,O) . b = 0. L )
assume A1: b <> HT p,O ; :: thesis: (HM p,O) . b = 0. L

per cases ( Support (HM p,O) = {} or ex b being bag of n st Support (HM p,O) = {b} ) by POLYNOM7:6;

suppose Support (HM p,O) = {} ; :: thesis: (HM p,O) . b = 0. L

then HM p,O = 0_ n,L by POLYNOM7:1;
hence (HM p,O) . b = 0. L by POLYNOM1:81; :: thesis: verum

end;

suppose ex b being bag of n st Support (HM p,O) = {b} ; :: thesis: (HM p,O) . b = 0. L

then consider b1 being bag of n such that
A2: Support (HM p,O) = {b1} ;
A3: b is Element of Bags n by PRE_POLY:def 12;

now

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

case HC p,O <> 0. L ; :: thesis: (HM p,O) . b = 0. L

then HT p,O in {b1} by A2, Lm9;
then b1 <> b by A1, TARSKI:def 1;
then not b in {b1} by TARSKI:def 1;
hence (HM p,O) . b = 0. L by A2, A3, POLYNOM1:def 9; :: thesis: verum

end;

case HC p,O = 0. L ; :: thesis: (HM p,O) . b = 0. L

then Support (HM p,O) = {} by Lm10;
then HM p,O = 0_ n,L by POLYNOM7:1;
hence (HM p,O) . b = 0. L by POLYNOM1:81; :: thesis: verum

end;

end;

end;

hence (HM p,O) . b = 0. L ; :: thesis: verum

end;

end;