theorem Th8: :: GROEB_3:8

for n being Ordinal
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for b being bag of n holds
( b in Support p iff (term m) + b in Support (m *' p) )