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

now

let u be set ; :: thesis: ( u in Support (HM p,O) implies u in Support p )
assume A1: u in Support (HM p,O) ; :: thesis: u in Support p

now

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

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

end;

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

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

end;

end;

end;

hence u in Support p ; :: thesis: verum

end;

end;

end;

hence u in Support p ; :: thesis: verum

end;

hence Support (HM p,O) c= Support p by TARSKI:def 3; :: thesis: verum