theorem Th40: :: GROEB_3:40

for n being Ordinal
for T being connected admissible TermOrder of n
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 i being Element of NAT st i <= card (Support p) holds
for b being bag of n holds
( (term m) + b in Support (Low ((m *' p),T,i)) iff b in Support (Low (p,T,i)) )