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 S_{1}[ 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;

_{1}[1]

S_{1}[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

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 S

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 & S_{1}[k] holds

S_{1}[k + 1]

A62:
SS

let k be Nat; :: thesis: ( 1 <= k & S_{1}[k] implies S_{1}[k + 1] )

assume A5: 1 <= k ; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

thus ( S_{1}[k] implies S_{1}[k + 1] )
:: thesis: verum

end;assume A5: 1 <= k ; :: thesis: ( S

thus ( S

proof

assume A6:
S_{1}[k]
; :: thesis: S_{1}[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 ) ) )_{1}[k + 1]
; :: thesis: verum

end;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

hence
S
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 A11, FINSEQ_1:17;

A14: dom R = Seg (k + 1) by A11, FINSEQ_1:def 3;

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:1;

then A23: Q . 1 = f by A9, FUNCT_1:47;

1 <= k + 1 by NAT_1:11;

then A24: k + 1 in dom R by A14, FINSEQ_1:1;

k in dom R by A5, A14, A12, FINSEQ_1:1;

then A25: [(R . k),(R . (k + 1))] in PolyRedRel (P,T) by A24, REWRITE1:def 2;

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 A26, XTUPLE_0:1;

reconsider g2 = g2 as Polynomial of n,L by A28, POLYNOM1:def 11;

not h9 in {(0_ (n,L))} by A3, A27, XBOOLE_0:def 5;

then h9 <> 0_ (n,L) by TARSKI:def 1;

then reconsider h9 = h9 as non-zero Polynomial of n,L by A27, POLYNOM1:def 11, POLYNOM7:def 1;

A30: Q . k = h9 by A5, A13, A29, FINSEQ_1:3, FUNCT_1:47;

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 A11, A12, FINSEQ_1:17;

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 A6, A7, A11, A12, A23, FINSEQ_1:17;

A33: k in dom Q by A5, A13, FINSEQ_1:3;

( 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;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 A11, FINSEQ_1:17;

A14: dom R = Seg (k + 1) by A11, FINSEQ_1:def 3;

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)

len Q = k
by A11, A12, FINSEQ_1:17;[(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 A13, A17, FINSEQ_1:1;

then A18: i + 1 <= k + 1 by A12, XXREAL_0:2;

i <= k by A13, A16, FINSEQ_1:1;

then A19: i <= k + 1 by A12, XXREAL_0:2;

1 <= i + 1 by A13, A17, FINSEQ_1:1;

then A20: i + 1 in dom R by A14, A18, FINSEQ_1:1;

1 <= i by A13, A16, FINSEQ_1:1;

then i in dom R by A14, A19, FINSEQ_1:1;

then A21: [(R . i),(R . (i + 1))] in PolyRedRel (P,T) by A20, REWRITE1:def 2;

R . i = Q . i by A16, FUNCT_1:47;

hence [(Q . i),(Q . (i + 1))] in PolyRedRel (P,T) by A17, A21, FUNCT_1:47; :: thesis: verum

end;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 A13, A17, FINSEQ_1:1;

then A18: i + 1 <= k + 1 by A12, XXREAL_0:2;

i <= k by A13, A16, FINSEQ_1:1;

then A19: i <= k + 1 by A12, XXREAL_0:2;

1 <= i + 1 by A13, A17, FINSEQ_1:1;

then A20: i + 1 in dom R by A14, A18, FINSEQ_1:1;

1 <= i by A13, A16, FINSEQ_1:1;

then i in dom R by A14, A19, FINSEQ_1:1;

then A21: [(R . i),(R . (i + 1))] in PolyRedRel (P,T) by A20, REWRITE1:def 2;

R . i = Q . i by A16, FUNCT_1:47;

hence [(Q . i),(Q . (i + 1))] in PolyRedRel (P,T) by A17, A21, FUNCT_1:47; :: thesis: verum

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:1;

then A23: Q . 1 = f by A9, FUNCT_1:47;

1 <= k + 1 by NAT_1:11;

then A24: k + 1 in dom R by A14, FINSEQ_1:1;

k in dom R by A5, A14, A12, FINSEQ_1:1;

then A25: [(R . k),(R . (k + 1))] in PolyRedRel (P,T) by A24, REWRITE1:def 2;

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 A26, XTUPLE_0:1;

reconsider g2 = g2 as Polynomial of n,L by A28, POLYNOM1:def 11;

not h9 in {(0_ (n,L))} by A3, A27, XBOOLE_0:def 5;

then h9 <> 0_ (n,L) by TARSKI:def 1;

then reconsider h9 = h9 as non-zero Polynomial of n,L by A27, POLYNOM1:def 11, POLYNOM7:def 1;

A30: Q . k = h9 by A5, A13, A29, FINSEQ_1:3, FUNCT_1:47;

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 A11, A12, FINSEQ_1:17;

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 A6, A7, A11, A12, A23, FINSEQ_1:17;

A33: k in dom Q by A5, A13, FINSEQ_1:3;

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 ) ) ) ) )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 ) ) ) ) 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 )
;

end;

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 ) ) )

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

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

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 ) ) )

( 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 A5, A33, A30, A22, A23, REWRITE1:17;

A36: R . (k + 1) = g2 by A26, XTUPLE_0:1;

then reconsider gg = g2 as Element of (Polynom-Ring (n,L)) by A8, A10, A11;

h9 reduces_to g2,P,T by A25, A26, POLYRED:def 13;

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 A38, GROEB_1:2;

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 A39, Lm3;

reconsider m9 = m9 as non-zero Monomial of n,L by A42, POLYNOM7:def 1;

reconsider p9 = p9 as non-zero Polynomial of n,L by A41, POLYNOM7:def 1;

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;

h9 is_reducible_wrt p9,T by A38, POLYRED:def 8;

then h9 <> 0_ (n,L) by POLYRED:37;

then HT (h9,T) <= HT (f,T),T by A35, POLYRED:44;

then A53: HT ((m9 *' p9),T) <= HT (f,T),T by A40, TERMORD:8;

( 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 A5, A13, A29, A31, FINSEQ_1:3, FUNCT_1:47 ;

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;A35: PolyRedRel (P,T) reduces f,h9 by A5, A33, A30, A22, A23, REWRITE1:17;

A36: R . (k + 1) = g2 by A26, XTUPLE_0:1;

then reconsider gg = g2 as Element of (Polynom-Ring (n,L)) by A8, A10, A11;

h9 reduces_to g2,P,T by A25, A26, POLYRED:def 13;

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 A38, GROEB_1:2;

A41: now :: thesis: not p9 = 0_ (n,L)

assume
p9 = 0_ (n,L)
; :: thesis: contradiction

then g2 = h9 - (0_ (n,L)) by A39, POLYRED:5

.= Q . k by A30, POLYRED:4 ;

hence contradiction by A8, A10, A11, A34, A36; :: thesis: verum

end;then g2 = h9 - (0_ (n,L)) by A39, POLYRED:5

.= Q . k by A30, POLYRED:4 ;

hence contradiction by A8, A10, A11, A34, A36; :: thesis: verum

A42: now :: thesis: not m9 = 0_ (n,L)

reconsider mp = m9 *' p9 as Element of (Polynom-Ring (n,L)) by POLYNOM1:def 11;assume
m9 = 0_ (n,L)
; :: thesis: contradiction

then g2 = h9 - (0_ (n,L)) by A39, POLYRED:5

.= Q . k by A30, POLYRED:4 ;

hence contradiction by A8, A10, A11, A34, A36; :: thesis: verum

end;then g2 = h9 - (0_ (n,L)) by A39, POLYRED:5

.= Q . k by A30, POLYRED:4 ;

hence contradiction by A8, A10, A11, A34, A36; :: thesis: verum

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 A39, Lm3;

reconsider m9 = m9 as non-zero Monomial of n,L by A42, POLYNOM7:def 1;

reconsider p9 = p9 as non-zero Polynomial of n,L by A41, POLYNOM7:def 1;

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

then reconsider B = A9 ^ <*mp*> as LeftLinearCombination of P by IDEAL_1:def 9;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 A44, A46, FINSEQ_1:1;

A48: 1 <= j by A44, A46, FINSEQ_1:1;

end;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 A44, A46, FINSEQ_1:1;

A48: 1 <= j by A44, A46, FINSEQ_1:1;

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 ) )end;

hence
ex u being Element of (Polynom-Ring (n,L)) ex a being Element of P st (A9 ^ <*mp*>) /. i = u * a
; :: thesis: verumper cases
( j = (len A9) + 1 or j <> (len A9) + 1 )
;

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 mp =
(A9 ^ <*mp*>) . j
by FINSEQ_1:42

.= (A9 ^ <*mp*>) /. j by A46, PARTFUN1:def 6 ;

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;.= (A9 ^ <*mp*>) /. j by A46, PARTFUN1:def 6 ;

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

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 A47, XXREAL_0:1;

then j <= len A9 by NAT_1:13;

then j in Seg (len A9) by A48, FINSEQ_1:1;

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 A46, PARTFUN1:def 6;

u9 * a9 = m *' p by POLYNOM1:def 11

.= (A9 ^ <*mp*>) /. j by A49, A51, A52, FINSEQ_1:def 7 ;

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 j <= len A9 by NAT_1:13;

then j in Seg (len A9) by A48, FINSEQ_1:1;

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 A46, PARTFUN1:def 6;

u9 * a9 = m *' p by POLYNOM1:def 11

.= (A9 ^ <*mp*>) /. j by A49, A51, A52, FINSEQ_1:def 7 ;

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

h9 is_reducible_wrt p9,T by A38, POLYRED:def 8;

then h9 <> 0_ (n,L) by POLYRED:37;

then HT (h9,T) <= HT (f,T),T by A35, POLYRED:44;

then A53: HT ((m9 *' p9),T) <= HT (f,T),T by A40, TERMORD:8;

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 )

take B = B; :: thesis: ex A being LeftLinearCombination of P st 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 A44, FINSEQ_1:1;

A57: 1 <= i by A44, A55, FINSEQ_1:1;

( p in P & B . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) ; :: thesis: verum

end;( 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 A44, FINSEQ_1:1;

A57: 1 <= i by A44, A55, FINSEQ_1:1;

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 ) ) )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 ) ) 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 )
;

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 )

( 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 A37, A53, FINSEQ_1:42; :: thesis: verum

end;( p in P & B . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) by A37, A53, FINSEQ_1:42; :: thesis: verum

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 )

( p in P & B . i = m *' p & HT ((m *' p),T) <= HT (f,T),T )

then
i < (len A9) + 1
by A56, XXREAL_0:1;

then i <= len A9 by NAT_1:13;

then i in Seg (len A9) by A57, FINSEQ_1:1;

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 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: verum

end;then i <= len A9 by NAT_1:13;

then i in Seg (len A9) by A57, FINSEQ_1:1;

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 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: verum

( p in P & B . i = m *' p & HT ((m *' p),T) <= HT (f,T),T ) ; :: thesis: verum

( 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 A5, A13, A29, A31, FINSEQ_1:3, FUNCT_1:47 ;

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

( 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

proof

A65:
for k being Nat st 1 <= k holds
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 A63, A64, RLVECT_1:def 4

.= 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;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 A63, A64, RLVECT_1:def 4

.= 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

S

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