theorem :: TERMORD:23

for n being Ordinal
for T being connected TermOrder of n
for L being non empty ZeroStr
for m being Monomial of n,L holds
( HT (m,T) = term m & HC (m,T) = coefficient m & HM (m,T) = m ) by Lm11;