let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (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 T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (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 L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (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 f, g be Polynomial of n,L; :: thesis: for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 holds
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (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 f9, g9 be Element of (Polynom-Ring (n,L)); :: thesis: ( f = f9 & g = g9 implies for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) ) )

assume A1: ( f = f9 & g = g9 ) ; :: thesis: for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) )

defpred S1[ Nat] means for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 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
( f9 = g9 + (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 (Polynom-Ring (n,L)); :: thesis: ( PolyRedRel (P,T) reduces f,g implies ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) ) )

assume PolyRedRel (P,T) reduces f,g ; :: thesis: ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) )

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 11;
A4: now :: thesis: for k being Nat st 1 <= k & S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( 1 <= k & S1[k] implies S1[k + 1] )
assume A5: 1 <= k ; :: thesis: ( S1[k] implies S1[k + 1] )
thus ( S1[k] implies S1[k + 1] ) :: thesis: verum
proof
assume A6: S1[k] ; :: thesis: S1[k + 1]
for f, g being Polynomial of n,L
for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 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
( f9 = g9 + (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: for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 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
( f9 = g9 + (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 f9, g9 be Element of (Polynom-Ring (n,L)); :: thesis: ( f = f9 & g = g9 implies 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
( f9 = g9 + (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 ) ) ) )

assume that
A7: f = f9 and
A8: g = g9 ; :: thesis: 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
( f9 = g9 + (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 (Polynom-Ring (n,L)); :: thesis: 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
( f9 = g9 + (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 R be RedSequence of PolyRedRel (P,T); :: thesis: ( R . 1 = f & R . (len R) = g & len R = k + 1 implies ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) ) )

assume that
A9: R . 1 = f and
A10: R . (len R) = g and
A11: len R = k + 1 ; :: thesis: ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) )

set Q = R | (Seg k);
reconsider Q = R | (Seg k) as FinSequence by FINSEQ_1:15;
A12: k <= k + 1 by NAT_1:11;
then A13: dom Q = Seg k by ;
A14: dom R = Seg (k + 1) by ;
A15: now :: thesis: for i being Nat st i in dom Q & i + 1 in dom Q holds
[(Q . i),(Q . (i + 1))] in PolyRedRel (P,T)
let i be Nat; :: thesis: ( i in dom Q & i + 1 in dom Q implies [(Q . i),(Q . (i + 1))] in PolyRedRel (P,T) )
assume that
A16: i in dom Q and
A17: i + 1 in dom Q ; :: thesis: [(Q . i),(Q . (i + 1))] in PolyRedRel (P,T)
i + 1 <= k by ;
then A18: i + 1 <= k + 1 by ;
i <= k by ;
then A19: i <= k + 1 by ;
1 <= i + 1 by ;
then A20: i + 1 in dom R by ;
1 <= i by ;
then i in dom R by ;
then A21: [(R . i),(R . (i + 1))] in PolyRedRel (P,T) by ;
R . i = Q . i by ;
hence [(Q . i),(Q . (i + 1))] in PolyRedRel (P,T) by ; :: thesis: verum
end;
len Q = k by ;
then reconsider Q = Q as RedSequence of PolyRedRel (P,T) by ;
A22: 1 in dom Q by ;
then A23: Q . 1 = f by ;
1 <= k + 1 by NAT_1:11;
then A24: k + 1 in dom R by ;
k in dom R by ;
then A25: [(R . k),(R . (k + 1))] in PolyRedRel (P,T) by ;
then consider h9, g2 being object such that
A26: [(R . k),(R . (k + 1))] = [h9,g2] and
A27: h9 in NonZero (Polynom-Ring (n,L)) and
A28: g2 in the carrier of (Polynom-Ring (n,L)) by RELSET_1:2;
A29: R . k = h9 by ;
reconsider g2 = g2 as Polynomial of n,L by ;
not h9 in {(0_ (n,L))} by ;
then h9 <> 0_ (n,L) by TARSKI:def 1;
then reconsider h9 = h9 as non-zero Polynomial of n,L by ;
A30: Q . k = h9 by ;
then reconsider u9 = Q . k as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider u = u9 as Polynomial of n,L by POLYNOM1:def 11;
Q . (len Q) = u by ;
then consider A9 being LeftLinearCombination of P such that
A31: f9 = u9 + (Sum A9) and
A32: for i being Element of NAT st i in dom A9 holds
ex m being non-zero Monomial of n,L ex p being non-zero Polynomial of n,L st
( p in P & A9 . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) by ;
A33: k in dom Q by ;
now :: thesis: ( ( u9 = g9 & ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) ) ) or ( u9 <> g9 & ex B, A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) ) ) )
per cases ( u9 = g9 or u9 <> g9 ) ;
case u9 = g9 ; :: thesis: ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) )

hence ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ; :: thesis: verum
end;
case A34: u9 <> g9 ; :: thesis: ex B, A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) )

reconsider hh = h9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A35: PolyRedRel (P,T) reduces f,h9 by ;
A36: R . (k + 1) = g2 by ;
then reconsider gg = g2 as Element of (Polynom-Ring (n,L)) by A8, A10, A11;
h9 reduces_to g2,P,T by ;
then consider p9 being Polynomial of n,L such that
A37: p9 in P and
A38: h9 reduces_to g2,p9,T by POLYRED:def 7;
consider m9 being Monomial of n,L such that
A39: g2 = h9 - (m9 *' p9) and
not HT ((m9 *' p9),T) in Support g2 and
A40: HT ((m9 *' p9),T) <= HT (h9,T),T by ;
A41: now :: thesis: not p9 = 0_ (n,L)
assume p9 = 0_ (n,L) ; :: thesis: contradiction
then g2 = h9 - (0_ (n,L)) by
.= Q . k by ;
hence contradiction by A8, A10, A11, A34, A36; :: thesis: verum
end;
A42: now :: thesis: not m9 = 0_ (n,L)
assume m9 = 0_ (n,L) ; :: thesis: contradiction
then g2 = h9 - (0_ (n,L)) by
.= Q . k by ;
hence contradiction by A8, A10, A11, A34, A36; :: thesis: verum
end;
reconsider mp = m9 *' p9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
reconsider pp = p9 as Element of P by A37;
set B = A9 ^ <*mp*>;
reconsider mm = m9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A43: gg = hh - mp by ;
reconsider m9 = m9 as non-zero Monomial of n,L by ;
reconsider p9 = p9 as non-zero Polynomial of n,L by ;
len (A9 ^ <*mp*>) = (len A9) + (len <*(m9 *' p9)*>) by FINSEQ_1:22
.= (len A9) + 1 by FINSEQ_1:40 ;
then A44: dom (A9 ^ <*mp*>) = Seg ((len A9) + 1) by FINSEQ_1:def 3;
A45: mp = mm * pp by POLYNOM1:def 11;
now :: thesis: for i being set st i in dom (A9 ^ <*mp*>) holds
ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a
let i be set ; :: thesis: ( i in dom (A9 ^ <*mp*>) implies ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a )
assume A46: i in dom (A9 ^ <*mp*>) ; :: thesis: ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a
then reconsider j = i as Element of NAT ;
A47: j <= (len A9) + 1 by ;
A48: 1 <= j by ;
now :: thesis: ( ( j = (len A9) + 1 & ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ) or ( j <> (len A9) + 1 & ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ) )
per cases ( j = (len A9) + 1 or j <> (len A9) + 1 ) ;
case j = (len A9) + 1 ; :: thesis: ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a
then mp = (A9 ^ <*mp*>) . j by FINSEQ_1:42
.= (A9 ^ <*mp*>) /. j by ;
hence ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a by A45; :: thesis: verum
end;
case j <> (len A9) + 1 ; :: thesis: ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a
then j < (len A9) + 1 by ;
then j <= len A9 by NAT_1:13;
then j in Seg (len A9) by ;
then A49: j in dom A9 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: A9 . j = m *' p and
HT ((m *' p),T) <= HT (f,T),T by A32;
reconsider a9 = p as Element of P by A50;
reconsider u9 = m as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;
A52: (A9 ^ <*mp*>) . j = (A9 ^ <*mp*>) /. j by ;
u9 * a9 = m *' p by POLYNOM1:def 11
.= (A9 ^ <*mp*>) /. j by ;
hence ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ; :: thesis: verum
end;
end;
end;
hence ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a ; :: thesis: verum
end;
then reconsider B = A9 ^ <*mp*> as LeftLinearCombination of P by IDEAL_1:def 9;
h9 is_reducible_wrt p9,T by ;
then h9 <> 0_ (n,L) by POLYRED:37;
then HT (h9,T) <= HT (f,T),T by ;
then A53: HT ((m9 *' p9),T) <= HT (f,T),T by ;
A54: now :: thesis: for i being Element of NAT st i in dom B holds
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 )
let i be Element of NAT ; :: thesis: ( i in dom B implies 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 ) )

assume A55: i in dom B ; :: thesis: 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 )

then A56: i <= (len A9) + 1 by ;
A57: 1 <= i by ;
now :: thesis: ( ( i = (len A9) + 1 & 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 ) ) or ( i <> (len A9) + 1 & 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 ) ) )
per cases ( i = (len A9) + 1 or i <> (len A9) + 1 ) ;
case i = (len A9) + 1 ; :: thesis: 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 )

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 ; :: thesis: verum
end;
case i <> (len A9) + 1 ; :: thesis: 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 )

then i < (len A9) + 1 by ;
then i <= len A9 by NAT_1:13;
then i in Seg (len A9) by ;
then A58: i in dom A9 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: A9 . i = m *' p and
A61: HT ((m *' p),T) <= HT (f,T),T by A32;
B . i = m *' p by ;
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 ; :: thesis: verum
end;
end;
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: verum
end;
take B = B; :: thesis: ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) )

gg + (Sum B) = gg + ((Sum A9) + (Sum <*mp*>)) by RLVECT_1:41
.= gg + ((Sum A9) + mp) by RLVECT_1:44
.= (hh + (- mp)) + ((Sum A9) + mp) by A43
.= hh + ((- mp) + ((Sum A9) + mp)) by RLVECT_1:def 3
.= hh + ((Sum A9) + ((- mp) + mp)) by RLVECT_1:def 3
.= hh + ((Sum A9) + (0. (Polynom-Ring (n,L)))) by RLVECT_1:5
.= hh + (Sum A9) by RLVECT_1:4
.= f9 by ;
hence ex A being LeftLinearCombination of P st
( f9 = g9 + (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: verum
end;
end;
end;
hence ex A being LeftLinearCombination of P st
( f9 = g9 + (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: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
end;
A62: S1
proof
set A = <*> the carrier of (Polynom-Ring (n,L));
let f, g be Polynomial of n,L; :: thesis: for f9, g9 being Element of (Polynom-Ring (n,L)) st f = f9 & g = g9 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
( f9 = g9 + (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 f9, g9 be Element of (Polynom-Ring (n,L)); :: thesis: ( f = f9 & g = g9 implies 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
( f9 = g9 + (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 ) ) ) )

assume A63: ( f = f9 & g = g9 ) ; :: thesis: 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
( f9 = g9 + (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 (Polynom-Ring (n,L)); :: thesis: 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
( f9 = g9 + (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 R be RedSequence of PolyRedRel (P,T); :: thesis: ( R . 1 = f & R . (len R) = g & len R = 1 implies ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) ) )

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 9;
assume A64: ( R . 1 = f & R . (len R) = g & len R = 1 ) ; :: thesis: ex A being LeftLinearCombination of P st
( f9 = g9 + (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 ) ) )

take A ; :: thesis: ( f9 = g9 + (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 ) ) )

f9 = g9 + (0. (Polynom-Ring (n,L))) by
.= g9 + (Sum A) by RLVECT_1:43 ;
hence ( f9 = g9 + (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: verum
end;
A65: for k being Nat st 1 <= k holds
S1[k] from NAT_1:sch 8(A62, A4);
1 <= len R by NAT_1:14;
hence ex A being LeftLinearCombination of P st
( f9 = g9 + (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: verum