let n be Ordinal; :: thesis: for T being connected TermOrder of n

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, g being Polynomial of n,L

for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, g being Polynomial of n,L

for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, g being Polynomial of n,L

for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let f, g be Polynomial of n,L; :: thesis: for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let P, Q be Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= Q & f reduces_to g,P,T implies f reduces_to g,Q,T )

assume A1: P c= Q ; :: thesis: ( not f reduces_to g,P,T or f reduces_to g,Q,T )

assume f reduces_to g,P,T ; :: thesis: f reduces_to g,Q,T

then ex p being Polynomial of n,L st

( p in P & f reduces_to g,p,T ) by POLYRED:def 7;

hence f reduces_to g,Q,T by A1, POLYRED:def 7; :: thesis: verum

for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, g being Polynomial of n,L

for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr

for f, g being Polynomial of n,L

for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, g being Polynomial of n,L

for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let f, g be Polynomial of n,L; :: thesis: for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds

f reduces_to g,Q,T

let P, Q be Subset of (Polynom-Ring (n,L)); :: thesis: ( P c= Q & f reduces_to g,P,T implies f reduces_to g,Q,T )

assume A1: P c= Q ; :: thesis: ( not f reduces_to g,P,T or f reduces_to g,Q,T )

assume f reduces_to g,P,T ; :: thesis: f reduces_to g,Q,T

then ex p being Polynomial of n,L st

( p in P & f reduces_to g,p,T ) by POLYRED:def 7;

hence f reduces_to g,Q,T by A1, POLYRED:def 7; :: thesis: verum