theorem Th26: :: TERMORD:26

for n being Ordinal
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)