theorem :: TERMORD:24

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for c being ConstPoly of n,L holds
( HT (c,T) = EmptyBag n & HC (c,T) = c . (EmptyBag n) )