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:22; :: 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 :: thesis: ( ( HC (p,O) <> 0. L & (HM (p,O)) . b = 0. L ) or ( HC (p,O) = 0. L & (HM (p,O)) . b = 0. L ) )

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

end;

end;

end;

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

end;

end;