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