theorem Th31: :: TERMORD:31

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being non-zero Polynomial of n,L holds HT ((p *' q),T) = (HT (p,T)) + (HT (q,T))