let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis:
let f, g be Polynomial of n,L; :: thesis:
let f', g' be Element of (Polynom-Ring n,L); :: thesis:
assume A1: ( f = f' & g = g' ) ; :: thesis:
let P be non empty Subset of (Polynom-Ring n,L); :: thesis:
assume A2: PolyRedRel P,T reduces f,g ; :: thesis:
X: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;
defpred S₁[ Nat] means for f, g being Polynomial of n,L
for f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' holds
for P being non empty Subset of (Polynom-Ring n,L)
for R being RedSequence of PolyRedRel P,T st R . 1 = f & R . (len R) = g & len R = $1 holds
ex A being LeftLinearCombination of P st
( f' = g' + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) );
A3: S₁[1]

proof

let f, g be Polynomial of n,L; :: thesis:
let f', g' be Element of (Polynom-Ring n,L); :: thesis:
assume A4: ( f = f' & g = g' ) ; :: thesis:
let P be non empty Subset of (Polynom-Ring n,L); :: thesis:
let R be RedSequence of PolyRedRel P,T; :: thesis:
assume A5: ( R . 1 = f & R . (len R) = g & len R = 1 ) ; :: thesis:
set A = <*> the carrier of (Polynom-Ring n,L);
for i being set st i in dom (<*> the carrier of (Polynom-Ring n,L)) holds
ex u being Element of (Polynom-Ring n,L) ex a being Element of P st (<*> the carrier of (Polynom-Ring n,L)) /. i = u * a ;
then reconsider A = <*> the carrier of (Polynom-Ring n,L) as LeftLinearCombination of P by IDEAL_1:def 10;
take A ; :: thesis:
f' = g' + (0. (Polynom-Ring n,L)) by A4, A5, RLVECT_1:def 7
.= g' + (Sum A) by RLVECT_1:60 ;
hence ( f' = g' + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) ) ; :: thesis:

end;

A7: now

let k be Nat; :: thesis:
assume A8: 1 <= k ; :: thesis:
thus ( S₁[k] implies S₁[k + 1] ) :: thesis:

proof

assume A9: S₁[k] ; :: thesis:
for f, g being Polynomial of n,L
for f', g' being Element of (Polynom-Ring n,L) st f = f' & g = g' holds
for P being non empty Subset of (Polynom-Ring n,L)
for R being RedSequence of PolyRedRel P,T st R . 1 = f & R . (len R) = g & len R = k + 1 holds
ex A being LeftLinearCombination of P st
( f' = g' + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) )

proof

let f, g be Polynomial of n,L; :: thesis:
let f', g' be Element of (Polynom-Ring n,L); :: thesis:
assume A10: ( f = f' & g = g' ) ; :: thesis:
let P be non empty Subset of (Polynom-Ring n,L); :: thesis:
let R be RedSequence of PolyRedRel P,T; :: thesis:
assume A11: ( R . 1 = f & R . (len R) = g & len R = k + 1 ) ; :: thesis:
then A12: dom R = Seg (k + 1) by FINSEQ_1:def 3;
A13: k <= k + 1 by NAT_1:11;
then A14: k in dom R by A8, A12, FINSEQ_1:3;
A15: 1 <= k + 1 by NAT_1:11;
set Q = R | (Seg k);
reconsider Q = R | (Seg k) as FinSequence by FINSEQ_1:19;
A16: len Q = k by A11, A13, FINSEQ_1:21;
A17: dom Q = Seg k by A11, A13, FINSEQ_1:21;

now

let i be Element of NAT ; :: thesis:
assume A18: ( i in dom Q & i + 1 in dom Q ) ; :: thesis:
then A19: ( 1 <= i & i <= k & 1 <= i + 1 & i + 1 <= k ) by A17, FINSEQ_1:3;
then A20: ( i <= k + 1 & i + 1 <= k + 1 ) by A13, XXREAL_0:2;
then A21: i in dom R by A12, A19, FINSEQ_1:3;
i + 1 in dom R by A12, A19, A20, FINSEQ_1:3;
then A22: [(R . i),(R . (i + 1))] in PolyRedRel P,T by A21, REWRITE1:def 2;
R . i = Q . i by A18, FUNCT_1:70;
hence [(Q . i),(Q . (i + 1))] in PolyRedRel P,T by A18, A22, FUNCT_1:70; :: thesis:

end;

then reconsider Q = Q as RedSequence of PolyRedRel P,T by A8, A16, REWRITE1:def 2;
k + 1 in dom R by A12, A15, FINSEQ_1:3;
then A23: [(R . k),(R . (k + 1))] in PolyRedRel P,T by A14, REWRITE1:def 2;
then consider h', g2 being set such that
A24: ( [(R . k),(R . (k + 1))] = [h',g2] & h' in NonZero (Polynom-Ring n,L) & g2 in the carrier of (Polynom-Ring n,L) ) by RELSET_1:6;
A25: R . k = [h',g2] `1 by A24, MCART_1:def 1
.= h' by MCART_1:def 1 ;
not h' in {(0_ n,L)} by A24, X, XBOOLE_0:def 5;
then h' <> 0_ n,L by TARSKI:def 1;
then reconsider h' = h' as non-zero Polynomial of n,L by A24, POLYNOM1:def 27, POLYNOM7:def 2;
reconsider g2 = g2 as Polynomial of n,L by A24, POLYNOM1:def 27;
A26: k in dom Q by A8, A17, FINSEQ_1:5;
then A27: Q . k = h' by A25, FUNCT_1:70;
then reconsider u' = Q . k as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider u = u' as Polynomial of n,L by POLYNOM1:def 27;
A28: 1 in dom Q by A8, A17, FINSEQ_1:3;
then A29: Q . 1 = f by A11, FUNCT_1:70;
Q . (len Q) = u by A11, A13, FINSEQ_1:21;
then consider A' being LeftLinearCombination of P such that
A30: ( f' = u' + (Sum A') & ( for i being Element of NAT st i in dom A' holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A' . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) ) by A9, A10, A16, A29;

now

per cases ;

case u' = g' ; :: thesis:

hence ex A being LeftLinearCombination of P st
( f' = g' + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) ) by A30; :: thesis:

end;

case A31: u' <> g' ; :: thesis:

h' reduces_to g2,P,T by A23, A24, POLYRED:def 13;
then consider p' being Polynomial of n,L such that
A32: ( p' in P & h' reduces_to g2,p',T ) by POLYRED:def 7;
consider m' being Monomial of n,L such that
A33: ( g2 = h' - (m' *' p') & not HT (m' *' p'),T in Support g2 & HT (m' *' p'),T <= HT h',T,T ) by A32, GROEB_1:2;
reconsider hh = h' as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
A34: R . (k + 1) = [h',g2] `2 by A24, MCART_1:def 2
.= g2 by MCART_1:def 2 ;
then reconsider gg = g2 as Element of (Polynom-Ring n,L) by A10, A11;
reconsider mm = m' as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider pp = p' as Element of P by A32;
reconsider mp = m' *' p' as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
A35: mp = mm * pp by POLYNOM1:def 27;

now

assume p' = 0_ n,L ; :: thesis:
then g2 = h' - (0_ n,L) by A33, POLYRED:5
.= Q . k by A27, POLYRED:4 ;
hence contradiction by A10, A11, A31, A34; :: thesis:

end;

then reconsider p' = p' as non-zero Polynomial of n,L by POLYNOM7:def 2;

now

assume m' = 0_ n,L ; :: thesis:
then g2 = h' - (0_ n,L) by A33, POLYRED:5
.= Q . k by A27, POLYRED:4 ;
hence contradiction by A10, A11, A31, A34; :: thesis:

end;

then reconsider m' = m' as non-zero Monomial of n,L by POLYNOM7:def 2;
A36: gg = hh - mp by A33, Lm3;
A37: PolyRedRel P,T reduces f,h' by A8, A26, A27, A28, A29, REWRITE1:18;
h' is_reducible_wrt p',T by A32, POLYRED:def 8;
then h' <> 0_ n,L by POLYRED:37;
then HT h',T <= HT f,T,T by A37, POLYRED:44;
then A38: HT (m' *' p'),T <= HT f,T,T by A33, TERMORD:8;
set B = A' ^ <*mp*>;
len (A' ^ <*mp*>) = (len A') + (len <*(m' *' p')*>) by FINSEQ_1:35
.= (len A') + 1 by FINSEQ_1:57 ;
then A39: dom (A' ^ <*mp*>) = Seg ((len A') + 1) by FINSEQ_1:def 3;

now

let i be set ; :: thesis:
assume A40: i in dom (A' ^ <*mp*>) ; :: thesis:
then reconsider j = i as Element of NAT ;
A41: ( 1 <= j & j <= (len A') + 1 ) by A39, A40, FINSEQ_1:3;

now

per cases ;

case j = (len A') + 1 ; :: thesis:

then mp = (A' ^ <*mp*>) . j by FINSEQ_1:59
.= (A' ^ <*mp*>) /. j by A40, PARTFUN1:def 8 ;
hence ex u being Element of (Polynom-Ring n,L) ex a being Element of P st (A' ^ <*mp*>) /. i = u * a by A35; :: thesis:

end;

case j <> (len A') + 1 ; :: thesis:

then j < (len A') + 1 by A41, XXREAL_0:1;
then j <= len A' by NAT_1:13;
then j in Seg (len A') by A41, FINSEQ_1:3;
then A42: j in dom A' by FINSEQ_1:def 3;
then consider m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A43: ( p in P & A' . j = m *' p & HT (m *' p),T <= HT f,T,T ) by A30;
A44: (A' ^ <*mp*>) . j = (A' ^ <*mp*>) /. j by A40, PARTFUN1:def 8;
reconsider u' = m as Element of (Polynom-Ring n,L) by POLYNOM1:def 27;
reconsider a' = p as Element of P by A43;
u' * a' = m *' p by POLYNOM1:def 27
.= (A' ^ <*mp*>) /. j by A42, A43, A44, FINSEQ_1:def 7 ;
hence ex u being Element of (Polynom-Ring n,L) ex a being Element of P st (A' ^ <*mp*>) /. i = u * a ; :: thesis:

end;

hence ex u being Element of (Polynom-Ring n,L) ex a being Element of P st (A' ^ <*mp*>) /. i = u * a ; :: thesis:

end;

then reconsider B = A' ^ <*mp*> as LeftLinearCombination of P by IDEAL_1:def 10;
take B = B; :: thesis:
A45: gg + (Sum B) = gg + ((Sum A') + (Sum <*mp*>)) by RLVECT_1:58
.= gg + ((Sum A') + mp) by RLVECT_1:61
.= (hh + (- mp)) + ((Sum A') + mp) by A36, RLVECT_1:def 12
.= hh + ((- mp) + ((Sum A') + mp)) by RLVECT_1:def 6
.= hh + ((Sum A') + ((- mp) + mp)) by RLVECT_1:def 6
.= hh + ((Sum A') + (0. (Polynom-Ring n,L))) by RLVECT_1:16
.= hh + (Sum A') by RLVECT_1:10
.= f' by A25, A26, A30, FUNCT_1:70 ;

now

let i be Element of NAT ; :: thesis:
assume i in dom B ; :: thesis:
then A46: ( 1 <= i & i <= (len A') + 1 ) by A39, FINSEQ_1:3;

now

per cases ;

case i = (len A') + 1 ; :: thesis:

hence ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B . i = m *' p & HT (m *' p),T <= HT f,T,T ) by A32, A38, FINSEQ_1:59; :: thesis:

end;

case i <> (len A') + 1 ; :: thesis:

then i < (len A') + 1 by A46, XXREAL_0:1;
then i <= len A' by NAT_1:13;
then i in Seg (len A') by A46, FINSEQ_1:3;
then A47: i in dom A' by FINSEQ_1:def 3;
then consider m being non-zero Monomial of n,L, p being non-zero Polynomial of n,L such that
A48: ( p in P & A' . i = m *' p & HT (m *' p),T <= HT f,T,T ) by A30;
B . i = m *' p by A47, A48, FINSEQ_1:def 7;
hence ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B . i = m *' p & HT (m *' p),T <= HT f,T,T ) by A48; :: thesis:

end;

hence ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & B . i = m *' p & HT (m *' p),T <= HT f,T,T ) ; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A49: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A3, A7);
consider R being RedSequence of PolyRedRel P,T such that
A50: ( R . 1 = f & R . (len R) = g ) by A2, REWRITE1:def 3;
len R > 0 by REWRITE1:def 2;
then 1 <= len R by NAT_1:14;
hence ex A being LeftLinearCombination of P st
( f' = g' + (Sum A) & ( for i being Element of NAT st i in dom A holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A . i = m *' p & HT (m *' p),T <= HT f,T,T ) ) ) by A1, A49, A50; :: thesis: