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 HT (HM p,T),T = HT p,T
let O be connected TermOrder of n; :: thesis: for L being non trivial ZeroStr
for p being Polynomial of n,L holds HT (HM p,O),O = HT p,O
let L be non trivial ZeroStr ; :: thesis: for p being Polynomial of n,L holds HT (HM p,O),O = HT p,O
let p be Polynomial of n,L; :: thesis: HT (HM p,O),O = HT p,O

per cases ( not HC p,O is zero or HC p,O is zero ) ;

suppose not HC p,O is zero ; :: thesis: HT (HM p,O),O = HT p,O

then reconsider a = HC p,O as non zero Element of L ;
thus HT (HM p,O),O = term (Monom a,(HT p,O)) by Lm11
.= HT p,O by POLYNOM7:10 ; :: thesis: verum

end;

suppose A1: HC p,O is zero ; :: thesis: HT (HM p,O),O = HT p,O

now

per cases ( not p is non-zero or p is non-zero ) ;

case not p is non-zero ; :: thesis: HT (HM p,O),O = HT p,O

then p = 0_ n,L by POLYNOM7:def 2;
then Support p = {} by POLYNOM7:1;
then HT p,O = EmptyBag n by Def6
.= term (Monom (0. L),(HT p,O)) by POLYNOM7:8
.= term (HM p,O) by A1, STRUCT_0:def 12 ;
hence HT (HM p,O),O = HT p,O by Lm11; :: thesis: verum

end;

case p is non-zero ; :: thesis: HT (HM p,O),O = HT p,O

then reconsider p = p as non-zero Polynomial of n,L ;
not HC p,O is zero ;
hence HT (HM p,O),O = HT p,O by A1; :: thesis: verum

end;

end;

end;

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

end;

end;