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 ; :: thesis:
assume A1: ( f = f' & g = g' ) ; :: thesis:
defpred S₁[ Nat] means for f, g being Polynomial of n,L
for f', g' being Element of st f = f' & g = g' holds
for P being non empty Subset of
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 ) ) );
let P be non empty Subset of ; :: thesis:
assume PolyRedRel P,T reduces f,g ; :: thesis:
then consider R being RedSequence of PolyRedRel P,T such that
A2: ( R . 1 = f & R . (len R) = g ) by REWRITE1:def 3;
A3: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;

A4: now

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

proof

assume A6: S₁[k] ; :: thesis:
for f, g being Polynomial of n,L
for f', g' being Element of st f = f' & g = g' holds
for P being non empty Subset of
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 ; :: thesis:
assume that
A7: f = f' and
A8: g = g' ; :: thesis:
let P be non empty Subset of ; :: thesis:
let R be RedSequence of PolyRedRel P,T; :: thesis:
assume that
A9: R . 1 = f and
A10: R . (len R) = g and
A11: len R = k + 1 ; :: thesis:
set Q = R | (Seg k);
reconsider Q = R | (Seg k) as FinSequence by FINSEQ_1:19;
A12: k <= k + 1 by NAT_1:11;
then A13: dom Q = Seg k by A11, FINSEQ_1:21;
A14: dom R = Seg (k + 1) by A11, FINSEQ_1:def 3;

A15: now

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

end;

len Q = k by A11, A12, FINSEQ_1:21;
then reconsider Q = Q as RedSequence of PolyRedRel P,T by A5, A15, REWRITE1:def 2;
A22: 1 in dom Q by A5, A13, FINSEQ_1:3;
then A23: Q . 1 = f by A9, FUNCT_1:70;
1 <= k + 1 by NAT_1:11;
then A24: k + 1 in dom R by A14, FINSEQ_1:3;
k in dom R by A5, A14, A12, FINSEQ_1:3;
then A25: [(R . k),(R . (k + 1))] in PolyRedRel P,T by A24, REWRITE1:def 2;
then consider h', g2 being set such that
A26: [(R . k),(R . (k + 1))] = [h',g2] and
A27: h' in NonZero (Polynom-Ring n,L) and
A28: g2 in the carrier of (Polynom-Ring n,L) by RELSET_1:6;
A29: R . k = [h',g2] `1 by A26, MCART_1:def 1
.= h' by MCART_1:def 1 ;
reconsider g2 = g2 as Polynomial of n,L by A28, POLYNOM1:def 27;
not h' in {(0_ n,L)} by A3, A27, 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 A27, POLYNOM1:def 27, POLYNOM7:def 2;
A30: Q . k = h' by A5, A13, A29, FINSEQ_1:5, FUNCT_1:70;
then reconsider u' = Q . k as Element of by POLYNOM1:def 27;
reconsider u = u' as Polynomial of n,L by POLYNOM1:def 27;
Q . (len Q) = u by A11, A12, FINSEQ_1:21;
then consider A' being LeftLinearCombination of P such that
A31: f' = u' + (Sum A') and
A32: 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 A6, A7, A11, A12, A23, FINSEQ_1:21;
A33: k in dom Q by A5, A13, FINSEQ_1:5;

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 A31, A32; :: thesis:

end;

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

reconsider hh = h' as Element of by POLYNOM1:def 27;
A35: PolyRedRel P,T reduces f,h' by A5, A33, A30, A22, A23, REWRITE1:18;
A36: R . (k + 1) = [h',g2] `2 by A26, MCART_1:def 2
.= g2 by MCART_1:def 2 ;
then reconsider gg = g2 as Element of by A8, A10, A11;
h' reduces_to g2,P,T by A25, A26, POLYRED:def 13;
then consider p' being Polynomial of n,L such that
A37: p' in P and
A38: h' reduces_to g2,p',T by POLYRED:def 7;
consider m' being Monomial of n,L such that
A39: g2 = h' - (m' *' p') and
not HT (m' *' p'),T in Support g2 and
A40: HT (m' *' p'),T <= HT h',T,T by A38, GROEB_1:2;

A41: now

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

end;

A42: now

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

end;

reconsider mp = m' *' p' as Element of by POLYNOM1:def 27;
reconsider pp = p' as Element of P by A37;
set B = A' ^ <*mp*>;
reconsider mm = m' as Element of by POLYNOM1:def 27;
A43: gg = hh - mp by A39, Lm3;
reconsider m' = m' as non-zero Monomial of n,L by A42, POLYNOM7:def 2;
reconsider p' = p' as non-zero Polynomial of n,L by A41, POLYNOM7:def 2;
len (A' ^ <*mp*>) = (len A') + (len <*(m' *' p')*>) by FINSEQ_1:35
.= (len A') + 1 by FINSEQ_1:57 ;
then A44: dom (A' ^ <*mp*>) = Seg ((len A') + 1) by FINSEQ_1:def 3;
A45: mp = mm * pp by POLYNOM1:def 27;

now

let i be set ; :: thesis:
assume A46: i in dom (A' ^ <*mp*>) ; :: thesis:
then reconsider j = i as Element of NAT ;
A47: j <= (len A') + 1 by A44, A46, FINSEQ_1:3;
A48: 1 <= j by A44, A46, 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 A46, PARTFUN1:def 8 ;
hence ex u being Element of ex a being Element of P st (A' ^ <*mp*>) /. i = u * a by A45; :: thesis:

end;

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

then j < (len A') + 1 by A47, XXREAL_0:1;
then j <= len A' by NAT_1:13;
then j in Seg (len A') by A48, FINSEQ_1:3;
then A49: 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
A50: p in P and
A51: A' . j = m *' p and
HT (m *' p),T <= HT f,T,T by A32;
reconsider a' = p as Element of P by A50;
reconsider u' = m as Element of by POLYNOM1:def 27;
A52: (A' ^ <*mp*>) . j = (A' ^ <*mp*>) /. j by A46, PARTFUN1:def 8;
u' * a' = m *' p by POLYNOM1:def 27
.= (A' ^ <*mp*>) /. j by A49, A51, A52, FINSEQ_1:def 7 ;
hence ex u being Element of ex a being Element of P st (A' ^ <*mp*>) /. i = u * a ; :: thesis:

end;

hence ex u being Element of 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;
h' is_reducible_wrt p',T by A38, POLYRED:def 8;
then h' <> 0_ n,L by POLYRED:37;
then HT h',T <= HT f,T,T by A35, POLYRED:44;
then A53: HT (m' *' p'),T <= HT f,T,T by A40, TERMORD:8;

A54: now

let i be Element of NAT ; :: thesis:
assume A55: i in dom B ; :: thesis:
then A56: i <= (len A') + 1 by A44, FINSEQ_1:3;
A57: 1 <= i by A44, A55, 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 A37, A53, FINSEQ_1:59; :: thesis:

end;

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

then i < (len A') + 1 by A56, XXREAL_0:1;
then i <= len A' by NAT_1:13;
then i in Seg (len A') by A57, FINSEQ_1:3;
then A58: 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
A59: p in P and
A60: A' . i = m *' p and
A61: HT (m *' p),T <= HT f,T,T by A32;
B . i = m *' p by A58, A60, 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 A59, A61; :: 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;

take B = B; :: thesis:
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 A43, 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 A5, A13, A29, A31, FINSEQ_1:5, FUNCT_1:70 ;
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 A8, A10, A11, A36, A54; :: thesis:

end;

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

end;

A62: S₁[1]

proof

set A = <*> the carrier of (Polynom-Ring n,L);
let f, g be Polynomial of n,L; :: thesis:
let f', g' be Element of ; :: thesis:
assume A63: ( f = f' & g = g' ) ; :: thesis:
let P be non empty Subset of ; :: thesis:
let R be RedSequence of PolyRedRel P,T; :: thesis:
for i being set st i in dom (<*> the carrier of (Polynom-Ring n,L)) holds
ex u being Element of 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;
assume A64: ( R . 1 = f & R . (len R) = g & len R = 1 ) ; :: thesis:
take A ; :: thesis:
f' = g' + (0. (Polynom-Ring n,L)) by A63, A64, 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;

A65: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A62, A4);
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, A65, A2; :: thesis: