theorem :: TERMORD:22

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
( term (HM (p,T)) = HT (p,T) & coefficient (HM (p,T)) = HC (p,T) )