theorem :: POLYRED:58

for n being Nat
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L))
for f, g being Element of (Polynom-Ring (n,L)) st f,g are_congruent_mod P -Ideal holds
f,g are_convertible_wrt PolyRedRel (P,T)