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 :: thesis: ( ( not p is non-zero & HT ((HM (p,O)),O) = HT (p,O) ) or ( p is non-zero & HT ((HM (p,O)),O) = HT (p,O) ) )

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