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 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 associative commutative well-unital distributive add-associative right_zeroed 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 associative commutative well-unital distributive add-associative right_zeroed 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 A1: ( PolyRedRel P,T reduces f,g & g <> f ) ; :: thesis: ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel P,T reduces h,g )
then consider p being RedSequence of PolyRedRel P,T such that
A2: ( p . 1 = f & p . (len p) = g ) by REWRITE1:def 3;
( len p > 0 & ( for i being Element of NAT st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in PolyRedRel P,T ) ) by REWRITE1:def 2;
then (len p) + 1 > 0 + 1 by XREAL_1:10;
then A3: 1 <= len p by NAT_1:13;
then 1 < len p by A1, A2, XXREAL_0:1;
then A4: 1 + 1 <= len p by NAT_1:13;
then A5: 1 + 1 in Seg (len p) by FINSEQ_1:3;
1 in Seg (len p) by A3, FINSEQ_1:3;
then A6: ( 1 in dom p & 1 + 1 in dom p ) by A5, FINSEQ_1:def 3;
set h = p . 2;
A7: [f,(p . 2)] in PolyRedRel P,T by A2, A6, REWRITE1:def 2;
then consider f', h' being set such that
A8: ( [f,(p . 2)] = [f',h'] & f' in NonZero (Polynom-Ring n,L) & h' in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
p . 2 = [f',h'] `2 by A8, MCART_1:def 2
.= h' by MCART_1:def 2 ;
then reconsider h = p . 2 as Polynomial of n,L by A8, POLYNOM1:def 27;
A9: f reduces_to h,P,T by A7, POLYRED:def 13;
len p in Seg (len p) by A3, FINSEQ_1:3;
then len p in dom p by FINSEQ_1:def 3;
hence ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel P,T reduces h,g ) by A2, A4, A6, A9, REWRITE1:18; :: thesis: verum