for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, f1, g, p being Polynomial of n,L st PolyRedRel ({p},T) reduces f,f1 & ( for b1 being bag of n st b1 in Support g holds
not HT (p,T) divides b1 ) holds
PolyRedRel ({p},T) reduces f + g,f1 + g