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 holds Support (HM (p,T)) c= Support p
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)) c= Support p
let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of n,L holds Support (HM (p,O)) c= Support p
let p be Polynomial of n,L; :: thesis: Support (HM (p,O)) c= Support p
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Support (HM (p,O)) or u in Support p )
assume A1: u in Support (HM (p,O)) ; :: thesis: u in Support p

now :: thesis: ( ( u in {} & u in Support p ) or ( u in {(HT (p,O))} & u in Support p ) )

per cases ( u in {} or u in {(HT (p,O))} ) by A1, Lm12;

case u in {} ; :: thesis: u in Support p

hence u in Support p ; :: thesis: verum

end;

case u in {(HT (p,O))} ; :: thesis: u in Support p

then A2: u = HT (p,O) by TARSKI:def 1;

now :: thesis: ( ( HC (p,O) = 0. L & contradiction ) or ( HC (p,O) <> 0. L & u in Support p ) )

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

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

then (HM (p,O)) . (HT (p,O)) = 0. L by Lm8;
hence contradiction by A1, A2, POLYNOM1:def 4; :: thesis: verum

end;

case HC (p,O) <> 0. L ; :: thesis: u in Support p

hence u in Support p by A2, POLYNOM1:def 4; :: thesis: verum

end;

end;

end;

hence u in Support p ; :: thesis: verum

end;

end;

end;

hence u in Support p ; :: thesis: verum