theorem :: TERMORD:40

for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for b being bag of n st b in Support p & b <> HT (p,T) holds
(Red (p,T)) . b = p . b by Lm19;