let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 consider p being Polynomial of n,L such that
A2: ( p in P & f reduces_to g,p,T ) by POLYRED:def 7;
thus f reduces_to g,Q,T by A1, A2, POLYRED:def 7; :: thesis: verum