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: now :: thesis: ( ( HC (p,O) <> 0. L & term (HM (p,O)) = HT (p,O) ) or ( HC (p,O) = 0. L & term (HM (p,O)) = HT (p,O) ) )

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 12;
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;

p . (HT (p,O)) = coefficient (HM (p,O)) by POLYNOM7:9
.= (HM (p,O)) . (term (HM (p,O))) by POLYNOM7:def 6 ;
hence (HM (p,O)) . (HT (p,O)) = p . (HT (p,O)) by A1; :: thesis: verum