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