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 being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )
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 being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )
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 being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )
let f, g be Polynomial of n,L; :: thesis: for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )
let P be Subset of (Polynom-Ring (n,L)); :: thesis: ( PolyRedRel (P,T) reduces f,g & g <> f implies ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g ) )
set R = PolyRedRel (P,T);
assume that
A1: PolyRedRel (P,T) reduces f,g and
A2: g <> f ; :: thesis: ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )
consider p being RedSequence of PolyRedRel (P,T) such that
A3: p . 1 = f and
A4: p . (len p) = g by A1, REWRITE1:def 3;
set h = p . 2;
len p > 0 ;
then (len p) + 1 > 0 + 1 by XREAL_1:8;
then A5: 1 <= len p by NAT_1:13;
then 1 < len p by A2, A3, A4, XXREAL_0:1;
then A6: 1 + 1 <= len p by NAT_1:13;
then 1 + 1 in Seg (len p) by FINSEQ_1:1;
then A7: 1 + 1 in dom p by FINSEQ_1:def 3;
1 in Seg (len p) by A5, FINSEQ_1:1;
then 1 in dom p by FINSEQ_1:def 3;
then A8: [f,(p . 2)] in PolyRedRel (P,T) by A3, A7, REWRITE1:def 2;
then consider f9, h9 being object such that
A9: [f,(p . 2)] = [f9,h9] and
f9 in NonZero (Polynom-Ring (n,L)) and
A10: h9 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
A11: p . 2 = h9 by A9, XTUPLE_0:1;
len p in Seg (len p) by A5, FINSEQ_1:1;
then A12: len p in dom p by FINSEQ_1:def 3;
reconsider h = p . 2 as Polynomial of n,L by A10, A11, POLYNOM1:def 11;
f reduces_to h,P,T by A8, POLYRED:def 13;
hence ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g ) by A4, A6, A7, A12, REWRITE1:17; :: thesis: verum