set cR = the carrier of R;
set PR = Polynom-Ring R;
set cPR = the carrier of (Polynom-Ring R);

now

assume not Polynom-Ring R is Noetherian ; :: thesis: contradiction
then consider I being Ideal of (Polynom-Ring R) such that
A1: not I is finitely_generated by IDEAL_1:def 26;
defpred S₁[ set , set , set ] means ( c₂ is non empty finite Subset of I implies ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = c₂ & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & c₃ = c₂ \/ {r} ) ) );

A2: now

let n be Element of NAT ; :: thesis: for x being Subset of the carrier of (Polynom-Ring R) ex y being Subset of the carrier of (Polynom-Ring R) st S₁[y,b₃,b₄]
let x be Subset of the carrier of (Polynom-Ring R); :: thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S₁[y,b₂,b₃]

per cases ( not x is non empty finite Subset of I or x is non empty finite Subset of I ) ;

suppose x is not non empty finite Subset of I ; :: thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S₁[y,b₂,b₃]

hence ex y being Subset of the carrier of (Polynom-Ring R) st S₁[n,x,y] ; :: thesis: verum

end;

suppose A3: x is non empty finite Subset of I ; :: thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S₁[y,b₂,b₃]

then reconsider x9 = x as non empty Subset of the carrier of (Polynom-Ring R) ;
set B = I \ (x9 -Ideal);

now

assume I \ (x9 -Ideal) = {} ; :: thesis: contradiction
then A4: I c= x9 -Ideal by XBOOLE_1:37;
x9 -Ideal c= I -Ideal by A3, IDEAL_1:57;
then x9 -Ideal c= I by IDEAL_1:44;
hence contradiction by A1, A3, A4, XBOOLE_0:def 10; :: thesis: verum

end;

then reconsider B = I \ (x9 -Ideal) as non empty Subset of the carrier of (Polynom-Ring R) ;
consider r being set such that
A5: r in minlen B by XBOOLE_0:def 1;
minlen B c= the carrier of (Polynom-Ring R) by XBOOLE_1:1;
then reconsider r = r as Element of the carrier of (Polynom-Ring R) by A5;
S₁[n,x,x9 \/ {r}] by A5;
hence ex y being Subset of the carrier of (Polynom-Ring R) st S₁[n,x,y] ; :: thesis: verum

end;

end;

end;

consider F being Function of NAT,(bool the carrier of (Polynom-Ring R)) such that
A6: ( F . 0 = {(0. (Polynom-Ring R))} & ( for n being Element of NAT holds S₁[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
defpred S₂[ set , set ] means ex n being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . n & B = I \ (A -Ideal) & n = R & F . (n + 1) = (F . n) \/ {c₂} & c₂ in minlen B );
defpred S₃[ Element of NAT ] means F . R is non empty finite Subset of I;

A7: now

let n be Element of NAT ; :: thesis: ( S₃[n] implies S₃[n + 1] )
assume S₃[n] ; :: thesis: S₃[n + 1]
then reconsider Fn = F . n as non empty finite Subset of I ;
consider A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A = Fn and
A8: B = I \ (A -Ideal) and
A9: ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . (n + 1) = Fn \/ {r} ) by A6;
consider r being Element of the carrier of (Polynom-Ring R) such that
A10: r in minlen B and
A11: F . (n + 1) = Fn \/ {r} by A9;
r in I by A8, A10, XBOOLE_0:def 5;
then {r} c= I by ZFMISC_1:31;
hence S₃[n + 1] by A11, XBOOLE_1:8; :: thesis: verum

end;

F . 0 c= I

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F . 0 or x in I )
assume x in F . 0 ; :: thesis: x in I
then x = 0. (Polynom-Ring R) by A6, TARSKI:def 1;
hence x in I by IDEAL_1:2; :: thesis: verum

end;

then A12: S₃[ 0 ] by A6;
A13: for n being Element of NAT holds S₃[n] from NAT_1:sch 1(A12, A7);

A14: now

let x be Element of NAT ; :: thesis: ex y being Element of the carrier of (Polynom-Ring R) st S₂[x,y]
ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . x & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . (x + 1) = (F . x) \/ {r} ) ) by A6, A13;
hence ex y being Element of the carrier of (Polynom-Ring R) st S₂[x,y] ; :: thesis: verum

end;

consider f being Function of NAT, the carrier of (Polynom-Ring R) such that
A15: for x being Element of NAT holds S₂[x,f . x] from FUNCT_2:sch 3(A14);
A16: for i, j being Element of NAT st i <= j holds
F . i c= F . j

proof

let i, j be Element of NAT ; :: thesis: ( i <= j implies F . i c= F . j )
defpred S₄[ Element of NAT ] means F . i c= F . (i + R);
assume i <= j ; :: thesis: F . i c= F . j
then consider m being Nat such that
A17: j = i + m by NAT_1:10;
A18: for m being Element of NAT st S₄[m] holds
S₄[m + 1]

proof

let m be Element of NAT ; :: thesis: ( S₄[m] implies S₄[m + 1] )
ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . (i + m) & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st
( r in minlen B & F . ((i + m) + 1) = (F . (i + m)) \/ {r} ) ) by A6, A13;
then A19: F . (i + m) c= F . ((i + m) + 1) by XBOOLE_1:7;
assume F . i c= F . (i + m) ; :: thesis: S₄[m + 1]
hence S₄[m + 1] by A19, XBOOLE_1:1; :: thesis: verum

end;

A20: S₄[ 0 ] ;
A21: for m being Element of NAT holds S₄[m] from NAT_1:sch 1(A20, A18);
m in NAT by ORDINAL1:def 12;
hence F . i c= F . j by A17, A21; :: thesis: verum

end;

A22: for i being Element of NAT holds f . i <> 0. (Polynom-Ring R)

proof

let i be Element of NAT ; :: thesis: f . i <> 0. (Polynom-Ring R)
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A23: A = F . n and
A24: B = I \ (A -Ideal) and
n = i and
F . (n + 1) = (F . n) \/ {(f . i)} and
A25: f . i in minlen B by A15;
F . n c= A -Ideal by A23, IDEAL_1:def 14;
then A26: not f . i in F . n by A24, A25, XBOOLE_0:def 5;
( F . 0 c= F . n & 0. (Polynom-Ring R) in F . 0 ) by A6, A16, TARSKI:def 1;
hence f . i <> 0. (Polynom-Ring R) by A26; :: thesis: verum

end;

A27: now

let i be Element of NAT ; :: thesis: for fi being Polynomial of R st fi = f . i holds
(len fi) - 1 >= 0
let fi be Polynomial of R; :: thesis: ( fi = f . i implies (len fi) - 1 >= 0 )
assume fi = f . i ; :: thesis: (len fi) - 1 >= 0
then fi <> 0. (Polynom-Ring R) by A22;
then fi <> 0_. R by POLYNOM3:def 10;
then len fi <> 0 by POLYNOM4:5;
then len fi >= 0 + 1 by NAT_1:13;
hence (len fi) - 1 >= 0 by XREAL_1:19; :: thesis: verum

end;

defpred S₄[ set , set ] means ex n being Element of NAT ex A being Polynomial of R st
( n = R & A = f . n & c₂ = A . ((len A) -' 1) );

A28: now

let x be Element of NAT ; :: thesis: ex y being Element of the carrier of R st S₄[x,y]
reconsider fx = f . x as Polynomial of R by POLYNOM3:def 10;
fx . ((len fx) -' 1) is Element of the carrier of R ;
hence ex y being Element of the carrier of R st S₄[x,y] ; :: thesis: verum

end;

consider a being Function of NAT, the carrier of R such that
A29: for x being Element of NAT holds S₄[x,a . x] from FUNCT_2:sch 3(A28);
reconsider a = a as sequence of R ;
for B being non empty Subset of the carrier of R ex C being non empty finite Subset of the carrier of R st
( C c= B & C -Ideal = B -Ideal ) by IDEAL_1:96;
then consider m being Element of NAT such that
A30: a . (m + 1) in (rng (a | (m + 1))) -Ideal by IDEAL_1:97;
reconsider fm1 = f . (m + 1) as Polynomial of R by POLYNOM3:def 10;
defpred S₅[ set , set ] means ( ex u, v, w being Element of the carrier of R st
( R = (u * v) * w & v in rng (a | (Segm (m + 1))) ) implies ex x, y, z being Element of the carrier of (Polynom-Ring R) ex p being Polynomial of R st
( c₂ = p & p = (x * y) * z & R = p . ((len fm1) -' 1) & len p <= len fm1 & y in F . (m + 1) ) );
A31: ex n being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . n & B = I \ (A -Ideal) & n = m + 1 & F . (n + 1) = (F . n) \/ {(f . (m + 1))} & f . (m + 1) in minlen B ) by A15;
A32: for i, j being Element of NAT
for fi, fj being Polynomial of R st i <= j & fi = f . i & fj = f . j holds
len fi <= len fj

proof

let i, j be Element of NAT ; :: thesis: for fi, fj being Polynomial of R st i <= j & fi = f . i & fj = f . j holds
len fi <= len fj
let fi, fj be Polynomial of R; :: thesis: ( i <= j & fi = f . i & fj = f . j implies len fi <= len fj )
assume that
A33: i <= j and
A34: fi = f . i and
A35: fj = f . j ; :: thesis: len fi <= len fj
consider k being Nat such that
A36: j = i + k by A33, NAT_1:10;
defpred S₆[ Element of NAT ] means for fk being Polynomial of R st fk = f . (i + R) holds
len fi <= len fk;

A37: now

let k be Element of NAT ; :: thesis: ( S₆[k] implies S₆[k + 1] )
assume A38: S₆[k] ; :: thesis: S₆[k + 1]

now

reconsider fk = f . (i + k) as Polynomial of R by POLYNOM3:def 10;
let fk1 be Polynomial of R; :: thesis: ( fk1 = f . (i + (k + 1)) implies len fi <= len fk1 )
A39: len fi <= len fk by A38;
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A40: A = F . n and
A41: B = I \ (A -Ideal) and
A42: n = i + k and
F . (n + 1) = (F . n) \/ {(f . (i + k))} and
A43: f . (i + k) in minlen B by A15;
consider n9 being Element of NAT , A9, B9 being non empty Subset of the carrier of (Polynom-Ring R) such that
A44: A9 = F . n9 and
A45: B9 = I \ (A9 -Ideal) and
A46: n9 = i + (k + 1) and
F . (n9 + 1) = (F . n9) \/ {(f . (i + (k + 1)))} and
A47: f . (i + (k + 1)) in minlen B9 by A15;
A48: f . (i + (k + 1)) in I by A45, A47, XBOOLE_0:def 5;
i + (k + 1) = (i + k) + 1 ;
then i + k < i + (k + 1) by NAT_1:13;
then A -Ideal c= A9 -Ideal by A16, A40, A42, A44, A46, IDEAL_1:57;
then not f . (i + (k + 1)) in A -Ideal by A45, A47, XBOOLE_0:def 5;
then A49: f . (i + (k + 1)) in B by A41, A48, XBOOLE_0:def 5;
assume fk1 = f . (i + (k + 1)) ; :: thesis: len fi <= len fk1
then len fk <= len fk1 by A43, A49, Th17;
hence len fi <= len fk1 by A39, XXREAL_0:2; :: thesis: verum

end;

hence S₆[k + 1] ; :: thesis: verum

end;

A50: S₆[ 0 ] by A34;
A51: for k being Element of NAT holds S₆[k] from NAT_1:sch 1(A50, A37);
k in NAT by ORDINAL1:def 12;
hence len fi <= len fj by A35, A36, A51; :: thesis: verum

end;

A52: for e being set st e in the carrier of R holds
ex d being set st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] )

proof

let e be set ; :: thesis: ( e in the carrier of R implies ex d being set st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] ) )
assume e in the carrier of R ; :: thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] )

per cases ( ex u, v, w being Element of the carrier of R st
( e = (u * v) * w & v in rng (a | (Segm (m + 1))) ) or for u, v, w being Element of the carrier of R holds
( not e = (u * v) * w or not v in rng (a | (Segm (m + 1))) ) ) ;

suppose ex u, v, w being Element of the carrier of R st
( e = (u * v) * w & v in rng (a | (Segm (m + 1))) ) ; :: thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] )

then consider u, b9, w being Element of the carrier of R such that
A53: e = (u * b9) * w and
A54: b9 in rng (a | (Segm (m + 1))) ;
consider n being set such that
A55: n in dom (a | (Segm (m + 1))) and
A56: b9 = (a | (Segm (m + 1))) . n by A54, FUNCT_1:def 3;
set c9 = w;
set a9 = u;
set z9 = monomial (w,0);
A57: (len fm1) -' 1 = ((len fm1) -' 1) + 0 ;
reconsider n = n as Element of NAT by A55;
set y = f . n;
reconsider y9 = f . n as Polynomial of R by POLYNOM3:def 10;
set x9 = monomial (u,((len fm1) -' (len y9)));
dom (a | (Segm (m + 1))) = (dom a) /\ (Segm (m + 1)) by RELAT_1:61
.= NAT /\ (Segm (m + 1)) by FUNCT_2:def 1
.= Segm (m + 1) by XBOOLE_1:28 ;
then A58: n < m + 1 by A55, NAT_1:44;
then len y9 <= len fm1 by A32;
then (len y9) - (len y9) <= (len fm1) - (len y9) by XREAL_1:9;
then A59: (len fm1) -' (len y9) = (len fm1) - (len y9) by XREAL_0:def 2;
then len (monomial (u,((len fm1) -' (len y9)))) <= ((len fm1) - (len y9)) + 1 by Th18;
then A60: (len (monomial (u,((len fm1) -' (len y9))))) + ((len y9) - 1) <= ((len fm1) - ((len y9) - 1)) + ((len y9) - 1) by XREAL_1:6;
A61: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= ((len (monomial (u,((len fm1) -' (len y9))))) + (len y9)) -' 1 by Th21;
A62: (len y9) - 1 >= 0 by A27;
then 0 + 0 <= ((len y9) - 1) + (len (monomial (u,((len fm1) -' (len y9))))) ;
then len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= ((len (monomial (u,((len fm1) -' (len y9))))) + (len y9)) - 1 by A61, XREAL_0:def 2;
then A63: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= len fm1 by A60, XXREAL_0:2;
(len fm1) - 1 >= 0 by A27;
then A64: (len fm1) -' 1 = ((len fm1) - (len y9)) + ((len y9) - 1) by XREAL_0:def 2
.= ((len y9) -' 1) + ((len fm1) -' (len y9)) by A59, A62, XREAL_0:def 2 ;
reconsider x = monomial (u,((len fm1) -' (len y9))), z = monomial (w,0) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
set p = (x * (f . n)) * z;
A65: x * (f . n) = (monomial (u,((len fm1) -' (len y9)))) *' y9 by POLYNOM3:def 10;
then A66: (x * (f . n)) * z = ((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0)) by POLYNOM3:def 10;
reconsider p = (x * (f . n)) * z as Polynomial of R by POLYNOM3:def 10;
A67: ex n9 being Element of NAT ex A being Polynomial of R st
( n9 = n & A = f . n9 & a . n = A . ((len A) -' 1) ) by A29;
b9 = a . n by A55, A56, FUNCT_1:47;
then ((monomial (u,((len fm1) -' (len y9)))) *' y9) . ((len fm1) -' 1) = u * b9 by A67, A64, Th19;
then A68: (u * b9) * w = p . ((len fm1) -' 1) by A66, A57, Th20;
ex n9 being Element of NAT ex A, B being non empty Subset of the carrier of (Polynom-Ring R) st
( A = F . n9 & B = I \ (A -Ideal) & n9 = n & F . (n9 + 1) = (F . n9) \/ {(f . n)} & f . n in minlen B ) by A15;
then {(f . n)} c= F . (n + 1) by XBOOLE_1:7;
then A69: f . n in F . (n + 1) by ZFMISC_1:31;
len (monomial (w,0)) <= 0 + 1 by Th18;
then (len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0))) <= (len fm1) + 1 by A63, XREAL_1:7;
then A70: ((len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0)))) -' 1 <= ((len fm1) + 1) -' 1 by NAT_D:42;
len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len ((monomial (u,((len fm1) -' (len y9)))) *' y9)) + (len (monomial (w,0)))) -' 1 by Th21;
then len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len fm1) + 1) -' 1 by A70, XXREAL_0:2;
then len (((monomial (u,((len fm1) -' (len y9)))) *' y9) *' (monomial (w,0))) <= ((len fm1) + 1) - 1 by XREAL_0:def 2;
then A71: len p <= (len fm1) + 0 by A65, POLYNOM3:def 10;
n + 1 <= m + 1 by A58, NAT_1:13;
then F . (n + 1) c= F . (m + 1) by A16;
hence ex d being set st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] ) by A53, A68, A71, A69; :: thesis: verum

end;

suppose for u, v, w being Element of the carrier of R holds
( not e = (u * v) * w or not v in rng (a | (Segm (m + 1))) ) ; :: thesis: ex d being set st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] )

hence ex d being set st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] ) ; :: thesis: verum

end;

end;

end;

consider LCT being Function of the carrier of R, the carrier of (Polynom-Ring R) such that
A72: for e being set st e in the carrier of R holds
S₅[e,LCT . e] from FUNCT_2:sch 1(A52);
reconsider FM1 = F . (m + 1) as non empty Subset of the carrier of (Polynom-Ring R) by A13;
set raSm1 = rng (a | (Segm (m + 1)));
consider lc being LinearCombination of rng (a | (Segm (m + 1))) such that
A73: a . (m + 1) = Sum lc by A30, IDEAL_1:60;
A74: for lc being LinearCombination of rng (a | (Segm (m + 1))) ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC )

proof

let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC )
set LC = LCT * lc;
dom LCT = the carrier of R by FUNCT_2:def 1;
then rng lc c= dom LCT ;
then A75: dom lc = dom (LCT * lc) by RELAT_1:27;
then A76: len lc = len (LCT * lc) by FINSEQ_3:29;
LCT * lc is LinearCombination of FM1

proof

let i be set ; :: according to IDEAL_1:def 8 :: thesis: ( not i in dom (LCT * lc) or ex b₁, b₂ being Element of the carrier of (Polynom-Ring R) ex b₃ being Element of FM1 st (LCT * lc) /. i = (b₁ * b₃) * b₂ )
assume A77: i in dom (LCT * lc) ; :: thesis: ex b₁, b₂ being Element of the carrier of (Polynom-Ring R) ex b₃ being Element of FM1 st (LCT * lc) /. i = (b₁ * b₃) * b₂
consider u, v being Element of R, a being Element of rng (a | (Segm (m + 1))) such that
A78: lc /. i = (u * a) * v by A75, A77, IDEAL_1:def 8;
A79: lc /. i = lc . i by A75, A77, PARTFUN1:def 6;
consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A80: ( LCT . (lc /. i) = p & p = (x * y) * z ) and
(u * a) * v = p . ((len fm1) -' 1) and
len p <= len fm1 and
A81: y in F . (m + 1) by A72, A78;
reconsider y = y as Element of FM1 by A81;
reconsider x = x, z = z as Element of (Polynom-Ring R) ;
(LCT * lc) /. i = (LCT * lc) . i by A77, PARTFUN1:def 6
.= (x * y) * z by A75, A77, A79, A80, FUNCT_1:13 ;
hence ex x, z being Element of (Polynom-Ring R) ex y being Element of FM1 st (LCT * lc) /. i = (x * y) * z ; :: thesis: verum

end;

then reconsider LC = LCT * lc as LinearCombination of FM1 ;
LC = LC ;
hence ex LC being LinearCombination of FM1 st
( LC = LCT * lc & len lc = len LC ) by A76; :: thesis: verum

end;

for lc being LinearCombination of rng (a | (Segm (m + 1))) ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

proof

let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
defpred S₆[ Element of NAT ] means for lc being LinearCombination of rng (a | (Segm (m + 1))) st len lc <= R holds
ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 );
A82: ex n being Element of NAT st n = len lc ;
A83: for k being Element of NAT st S₆[k] holds
S₆[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₆[k] implies S₆[k + 1] )
assume A84: S₆[k] ; :: thesis: S₆[k + 1]
thus S₆[k + 1] :: thesis: verum

proof

let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ( len lc <= k + 1 implies ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) )
assume A85: len lc <= k + 1 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

per cases ( len lc <= k or len lc > k ) ;

suppose len lc <= k ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A84; :: thesis: verum

end;

suppose A86: len lc > k ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

then len lc >= k + 1 by NAT_1:13;
then A87: len lc = k + 1 by A85, XXREAL_0:1;
thus ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) :: thesis: verum

proof

per cases ( k = 0 or k > 0 ) ;

suppose A88: k = 0 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

then dom lc = {1} by A87, FINSEQ_1:2, FINSEQ_1:def 3;
then A89: 1 in dom lc by TARSKI:def 1;
then consider u, w being Element of R, v being Element of rng (a | (Segm (m + 1))) such that
A90: lc /. 1 = (u * v) * w by IDEAL_1:def 8;
A91: lc . 1 = lc /. 1 by A89, PARTFUN1:def 6;
then consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A92: LCT . (lc . 1) = p and
p = (x * y) * z and
A93: (u * v) * w = p . ((len fm1) -' 1) and
A94: len p <= len fm1 and
y in F . (m + 1) by A72, A90;
A95: lc = <*(lc . 1)*> by A87, A88, FINSEQ_1:40;
then A96: Sum lc = p . ((len fm1) -' 1) by A90, A91, A93, RLVECT_1:44;
consider LC being LinearCombination of FM1 such that
A97: LC = LCT * lc and
len LC = len lc by A74;
LC = <*(LCT . ((u * v) * w))*> by A95, A90, A91, A97, FINSEQ_2:35;
then Sum LC = p by A90, A91, A92, RLVECT_1:44;
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A94, A97, A96; :: thesis: verum

end;

suppose A98: k > 0 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

consider LC being LinearCombination of FM1 such that
A99: LC = LCT * lc and
len LC = len lc by A74;
not lc is empty by A86;
then consider p being LinearCombination of rng (a | (Segm (m + 1))), e being Element of the carrier of R such that
A100: lc = p ^ <*e*> and
A101: <*e*> is LinearCombination of rng (a | (Segm (m + 1))) by IDEAL_1:32;
len <*e*> = 0 + 1 by FINSEQ_1:39;
then len <*e*> <= k by A98, NAT_1:13;
then consider LCe being LinearCombination of FM1, sLCe being Polynomial of R such that
A102: LCe = LCT * <*e*> and
A103: sLCe = Sum LCe and
A104: sLCe . ((len fm1) -' 1) = Sum <*e*> and
A105: len sLCe <= len fm1 by A84, A101;
len lc = (len p) + (len <*e*>) by A100, FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:39 ;
then consider LCp being LinearCombination of FM1, sLCp being Polynomial of R such that
A106: LCp = LCT * p and
A107: sLCp = Sum LCp and
A108: sLCp . ((len fm1) -' 1) = Sum p and
A109: len sLCp <= len fm1 by A84, A87;
set sLC = sLCp + sLCe;
A110: Sum lc = (Sum p) + e by A100, FVSUM_1:71
.= (sLCp . ((len fm1) -' 1)) + (sLCe . ((len fm1) -' 1)) by A108, A104, RLVECT_1:44
.= (sLCp + sLCe) . ((len fm1) -' 1) by NORMSP_1:def 2 ;

A111: now

per cases ( len sLCp < len sLCe or len sLCp >= len sLCe ) ;

suppose len sLCp < len sLCe ; :: thesis: len (sLCp + sLCe) <= len fm1

then len (sLCp + sLCe) <= len sLCe by POLYNOM4:6;
hence len (sLCp + sLCe) <= len fm1 by A105, XXREAL_0:2; :: thesis: verum

end;

suppose len sLCp >= len sLCe ; :: thesis: len (sLCp + sLCe) <= len fm1

then len (sLCp + sLCe) <= len sLCp by POLYNOM4:6;
hence len (sLCp + sLCe) <= len fm1 by A109, XXREAL_0:2; :: thesis: verum

end;

end;

end;

dom LCT = the carrier of R by FUNCT_2:def 1;
then (rng p) \/ (rng <*e*>) c= dom LCT ;
then ex LCTp, LCTe being FinSequence st
( LCTp = LCT * p & LCTe = LCT * <*e*> & LCT * (p ^ <*e*>) = LCTp ^ LCTe ) by Th1;
then Sum LC = (Sum LCp) + (Sum LCe) by A100, A106, A102, A99, RLVECT_1:41
.= sLCp + sLCe by A107, A103, POLYNOM3:def 10 ;
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A99, A110, A111; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

A112: S₆[ 0 ]

proof

let lc be LinearCombination of rng (a | (Segm (m + 1))); :: thesis: ( len lc <= 0 implies ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) )
assume A113: len lc <= 0 ; :: thesis: ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
then A114: lc = <*> the carrier of R ;
consider LC being LinearCombination of FM1 such that
A115: LC = LCT * lc and
A116: len lc = len LC by A74;
take LC ; :: thesis: ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )
take p = 0_. R; :: thesis: ( LC = LCT * lc & p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
thus LC = LCT * lc by A115; :: thesis: ( p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
LC = <*> the carrier of (Polynom-Ring R) by A113, A116;
then Sum LC = 0. (Polynom-Ring R) by RLVECT_1:43
.= p by POLYNOM3:def 10 ;
hence p = Sum LC ; :: thesis: ( p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
thus p . ((len fm1) -' 1) = 0. R by FUNCOP_1:7
.= Sum lc by A114, RLVECT_1:43 ; :: thesis: len p <= len fm1
thus len p <= len fm1 by POLYNOM4:3; :: thesis: verum

end;

for k being Element of NAT holds S₆[k] from NAT_1:sch 1(A112, A83);
hence ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A82; :: thesis: verum

end;

then consider LC being LinearCombination of FM1, sLC being Polynomial of R such that
LC = LCT * lc and
A117: sLC = Sum LC and
A118: sLC . ((len fm1) -' 1) = Sum lc and
A119: len sLC <= len fm1 ;
A120: sLC in FM1 -Ideal by A117, IDEAL_1:60;
set f9 = fm1 - sLC;

A121: now

ex n being Element of NAT ex A being Polynomial of R st
( n = m + 1 & A = f . n & a . (m + 1) = A . ((len A) -' 1) ) by A29;
then A122: (fm1 - sLC) . ((len fm1) -' 1) = (fm1 . ((len fm1) -' 1)) - (fm1 . ((len fm1) -' 1)) by A73, A118, POLYNOM3:27
.= 0. R by RLVECT_1:15 ;
(len fm1) - 1 >= 0 by A27;
then A123: ((len fm1) -' 1) + 1 = ((len fm1) - 1) + 1 by XREAL_0:def 2
.= len fm1 ;
assume len (fm1 - sLC) = len fm1 ; :: thesis: contradiction
hence contradiction by A123, A122, ALGSEQ_1:10; :: thesis: verum

end;

A124: (fm1 - sLC) + sLC = fm1 + (sLC + (- sLC)) by POLYNOM3:26
.= fm1 + (sLC - sLC)
.= fm1 + (0_. R) by POLYNOM3:29
.= fm1 by POLYNOM3:28 ;

A125: now

reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
assume A126: fm1 - sLC in FM1 -Ideal ; :: thesis: contradiction
reconsider f9 = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
f . (m + 1) = f9 + sLC by A124, POLYNOM3:def 10;
then fm1 in FM1 -Ideal by A120, A126, IDEAL_1:def 1;
hence contradiction by A31, XBOOLE_0:def 5; :: thesis: verum

end;

len (- sLC) <= len fm1 by A119, POLYNOM4:8;
then len (fm1 - sLC) <= len fm1 by POLYNOM4:6;
then A127: len (fm1 - sLC) < len fm1 by A121, XXREAL_0:1;
fm1 - sLC in I

proof

reconsider f9 = fm1 - sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
FM1 is Subset of I by A13;
then FM1 -Ideal c= I -Ideal by IDEAL_1:57;
then A128: FM1 -Ideal c= I by IDEAL_1:44;
( f . (m + 1) in I & f9 = (f . (m + 1)) - sLC ) by A31, Th16, XBOOLE_0:def 5;
hence fm1 - sLC in I by A120, A128, IDEAL_1:15; :: thesis: verum

end;

then fm1 - sLC in I \ (FM1 -Ideal) by A125, XBOOLE_0:def 5;
hence contradiction by A127, A31, Th17; :: thesis: verum

end;

hence Polynom-Ring R is Noetherian ; :: thesis: verum