theorem :: TERMORD:18

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 (HM (p,T)) . (HT (p,T)) = p . (HT (p,T)) by Lm8;