theorem :: POLYNOM9:26

for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R
for b being bag of O holds Support (p - (Monom ((p . b),b))) = (Support p) \ {b}