:: deftheorem defines HM TERMORD:def 8 :
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 (p,T) = Monom ((HC (p,T)),(HT (p,T)));