for n being Ordinal
for T being connected 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 P being Subset of (Polynom-Ring (n,L))
for f, g, h, h1 being Polynomial of n,L st f - g = h & PolyRedRel (P,T) reduces h,h1 holds
ex f1, g1 being Polynomial of n,L st
( f1 - g1 = h1 & PolyRedRel (P,T) reduces f,f1 & PolyRedRel (P,T) reduces g,g1 )