theorem Th15: :: POLYRED:15

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L
for b being bag of n holds HT ((b *' p),T) = b + (HT (p,T))