theorem :: POLYRED:39

for n being Ordinal
for T being connected TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L
for b being bag of n st f reduces_to g,p,b,T holds
not b in Support g by Lm17;