let n be Ordinal; for T being connected TermOrder of n
for L being non trivial ZeroStr
for p being Polynomial of n,L holds HC ((HM (p,T)),T) = HC (p,T)
let O be connected TermOrder of n; for L being non trivial ZeroStr
for p being Polynomial of n,L holds HC ((HM (p,O)),O) = HC (p,O)
let L be non trivial ZeroStr ; for p being Polynomial of n,L holds HC ((HM (p,O)),O) = HC (p,O)
let p be Polynomial of n,L; HC ((HM (p,O)),O) = HC (p,O)
thus HC ((HM (p,O)),O) =
(HM (p,O)) . (HT (p,O))
by Th26
.=
HC (p,O)
by Lm8
; verum