theorem :: TERMORD:28

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Polynomial of n,L holds HM ((HM (p,T)),T) = HM (p,T) by Lm11;