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 (HM p,O) . (HT p,O) = p . (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 (HM p,O) . (HT p,O) = p . (HT p,O)
let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of n,L holds (HM p,O) . (HT p,O) = p . (HT p,O)
let p be Polynomial of n,L; :: thesis: (HM p,O) . (HT p,O) = p . (HT p,O)
A1: p . (HT p,O) = coefficient (HM p,O) by POLYNOM7:9
.= (HM p,O) . (term (HM p,O)) by POLYNOM7:def 7 ;

now

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

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

then not HC p,O is zero by STRUCT_0:def 15;
hence term (HM p,O) = HT p,O by POLYNOM7:10; :: thesis: verum

end;

case A2: HC p,O = 0. L ; :: thesis: term (HM p,O) = HT p,O

then p = 0_ n,L by Lm7;
then Support p = {} by POLYNOM7:1;
then HT p,O = EmptyBag n by Def6;
hence term (HM p,O) = HT p,O by A2, POLYNOM7:8; :: thesis: verum

end;

end;

end;

hence (HM p,O) . (HT p,O) = p . (HT p,O) by A1; :: thesis: verum