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

now :: thesis: Polynom-Ring R is Noetherian

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 ;
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 :: thesis: for n being Nat
for x being Subset of the carrier of (Polynom-Ring R) ex y being Subset of the carrier of (Polynom-Ring R) st S₁[n,x,y]

let n be 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 :: thesis: not I \ (x9 -Ideal) = {}

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 object 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 sequence of (bool the carrier of (Polynom-Ring R)) such that
A6: ( F . 0 = {(0. (Polynom-Ring R))} & ( for n being 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₃[ Nat] means F . R is non empty finite Subset of I;

A7: now :: thesis: for n being Nat st S₃[n] holds
S₃[n + 1]

let n be 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 object ; :: 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 Nat holds S₃[n] from NAT_1:sch 2(A12, A7);

A14: now :: thesis: for x being Element of NAT ex y being Element of the carrier of (Polynom-Ring R) st S₂[x,y]

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 sequence of 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 x being Nat holds S₂[x,f . x]

proof

let n be Nat; :: thesis: S₂[n,f . n]
n in NAT by ORDINAL1:def 12;
hence S₂[n,f . n] by A15; :: thesis: verum

end;

A17: 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₄[ Nat] means F . i c= F . (i + R);
assume i <= j ; :: thesis: F . i c= F . j
then consider m being Nat such that
A18: j = i + m by NAT_1:10;
A19: for m being Nat st S₄[m] holds
S₄[m + 1]

proof

let m be 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 A20: 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 A20, XBOOLE_1:1; :: thesis: verum

end;

A21: S₄[ 0 ] ;
A22: for m being Nat holds S₄[m] from NAT_1:sch 2(A21, A19);
thus F . i c= F . j by A18, A22; :: thesis: verum

end;

A23: 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
A24: A = F . n and
A25: B = I \ (A -Ideal) and
n = i and
F . (n + 1) = (F . n) \/ {(f . i)} and
A26: f . i in minlen B by A16;
F . n c= A -Ideal by A24, IDEAL_1:def 14;
then A27: not f . i in F . n by A25, A26, XBOOLE_0:def 5;
( F . 0 c= F . n & 0. (Polynom-Ring R) in F . 0 ) by A6, A17, TARSKI:def 1;
hence f . i <> 0. (Polynom-Ring R) by A27; :: thesis: verum

end;

A28: now :: thesis: for i being Element of NAT
for fi being Polynomial of R st fi = f . i holds
(len fi) - 1 >= 0

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

A29: now :: thesis: for x being Element of NAT ex y being Element of the carrier of R st S₄[x,y]

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 sequence of the carrier of R such that
A30: for x being Element of NAT holds S₄[x,a . x] from FUNCT_2:sch 3(A29);
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
A31: 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₅[ object , object ] 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) ) );
A32: 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 A16;
A33: 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
A34: i <= j and
A35: fi = f . i and
A36: fj = f . j ; :: thesis: len fi <= len fj
consider k being Nat such that
A37: j = i + k by A34, NAT_1:10;
defpred S₆[ Nat] means for fk being Polynomial of R st fk = f . (i + R) holds
len fi <= len fk;

A38: now :: thesis: for k being Nat st S₆[k] holds
S₆[k + 1]

let k be Nat; :: thesis: ( S₆[k] implies S₆[k + 1] )
assume A39: S₆[k] ; :: thesis: S₆[k + 1]

now :: thesis: for fk1 being Polynomial of R st fk1 = f . (i + (k + 1)) holds
len fi <= len fk1

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 )
A40: len fi <= len fk by A39;
consider n being Element of NAT , A, B being non empty Subset of the carrier of (Polynom-Ring R) such that
A41: A = F . n and
A42: B = I \ (A -Ideal) and
A43: n = i + k and
F . (n + 1) = (F . n) \/ {(f . (i + k))} and
A44: f . (i + k) in minlen B by A16;
consider n9 being Element of NAT , A9, B9 being non empty Subset of the carrier of (Polynom-Ring R) such that
A45: A9 = F . n9 and
A46: B9 = I \ (A9 -Ideal) and
A47: n9 = i + (k + 1) and
F . (n9 + 1) = (F . n9) \/ {(f . (i + (k + 1)))} and
A48: f . (i + (k + 1)) in minlen B9 by A16;
A49: f . (i + (k + 1)) in I by A46, A48, 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 A17, A41, A43, A45, A47, IDEAL_1:57;
then not f . (i + (k + 1)) in A -Ideal by A46, A48, XBOOLE_0:def 5;
then A50: f . (i + (k + 1)) in B by A42, A49, XBOOLE_0:def 5;
assume fk1 = f . (i + (k + 1)) ; :: thesis: len fi <= len fk1
then len fk <= len fk1 by A44, A50, Th17;
hence len fi <= len fk1 by A40, XXREAL_0:2; :: thesis: verum

end;

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

end;

A51: S₆[ 0 ] by A35;
A52: for k being Nat holds S₆[k] from NAT_1:sch 2(A51, A38);
thus len fi <= len fj by A36, A37, A52; :: thesis: verum

end;

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

proof

let e be object ; :: thesis: ( e in the carrier of R implies ex d being object st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] ) )
assume e in the carrier of R ; :: thesis: ex d being object 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 object 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
A54: e = (u * b9) * w and
A55: b9 in rng (a | (Segm (m + 1))) ;
consider n being object such that
A56: n in dom (a | (Segm (m + 1))) and
A57: b9 = (a | (Segm (m + 1))) . n by A55, FUNCT_1:def 3;
set c9 = w;
set a9 = u;
set z9 = monomial (w,0);
A58: (len fm1) -' 1 = ((len fm1) -' 1) + 0 ;
reconsider n = n as Element of NAT by A56;
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 A59: n < m + 1 by A56, NAT_1:44;
then len y9 <= len fm1 by A33;
then (len y9) - (len y9) <= (len fm1) - (len y9) by XREAL_1:9;
then A60: (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 A61: (len (monomial (u,((len fm1) -' (len y9))))) + ((len y9) - 1) <= ((len fm1) - ((len y9) - 1)) + ((len y9) - 1) by XREAL_1:6;
A62: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= ((len (monomial (u,((len fm1) -' (len y9))))) + (len y9)) -' 1 by Th21;
A63: (len y9) - 1 >= 0 by A28;
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 A62, XREAL_0:def 2;
then A64: len ((monomial (u,((len fm1) -' (len y9)))) *' y9) <= len fm1 by A61, XXREAL_0:2;
(len fm1) - 1 >= 0 by A28;
then A65: (len fm1) -' 1 = ((len fm1) - (len y9)) + ((len y9) - 1) by XREAL_0:def 2
.= ((len y9) -' 1) + ((len fm1) -' (len y9)) by A60, A63, 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;
A66: x * (f . n) = (monomial (u,((len fm1) -' (len y9)))) *' y9 by POLYNOM3:def 10;
then A67: (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;
A68: 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 A30;
b9 = a . n by A56, A57, FUNCT_1:47;
then ((monomial (u,((len fm1) -' (len y9)))) *' y9) . ((len fm1) -' 1) = u * b9 by A68, A65, Th19;
then A69: (u * b9) * w = p . ((len fm1) -' 1) by A67, A58, 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 A16;
then {(f . n)} c= F . (n + 1) by XBOOLE_1:7;
then A70: 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 A64, XREAL_1:7;
then A71: ((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 A71, 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 A72: len p <= (len fm1) + 0 by A66, POLYNOM3:def 10;
n + 1 <= m + 1 by A59, NAT_1:13;
then F . (n + 1) c= F . (m + 1) by A17;
hence ex d being object st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] ) by A54, A69, A72, A70; :: 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 object st
( d in the carrier of (Polynom-Ring R) & S₅[e,d] )

hence ex d being object 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
A73: for e being object st e in the carrier of R holds
S₅[e,LCT . e] from FUNCT_2:sch 1(A53);
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
A74: a . (m + 1) = Sum lc by A31, IDEAL_1:60;
A75: 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 A76: dom lc = dom (LCT * lc) by RELAT_1:27;
then A77: 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 A78: 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
A79: lc /. i = (u * a) * v by A76, A78, IDEAL_1:def 8;
A80: lc /. i = lc . i by A76, A78, PARTFUN1:def 6;
consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A81: ( LCT . (lc /. i) = p & p = (x * y) * z ) and
(u * a) * v = p . ((len fm1) -' 1) and
len p <= len fm1 and
A82: y in F . (m + 1) by A73, A79;
reconsider y = y as Element of FM1 by A82;
reconsider x = x, z = z as Element of (Polynom-Ring R) ;
(LCT * lc) /. i = (LCT * lc) . i by A78, PARTFUN1:def 6
.= (x * y) * z by A76, A78, A80, A81, 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 A77; :: 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₆[ 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 );
A83: ex n being Element of NAT st n = len lc ;
A84: for k being Nat st S₆[k] holds
S₆[k + 1]

proof

let k be Nat; :: thesis: ( S₆[k] implies S₆[k + 1] )
assume A85: 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 A86: 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 A85; :: thesis: verum

end;

suppose A87: 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 A88: len lc = k + 1 by A86, 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 A89: 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 A88, FINSEQ_1:2, FINSEQ_1:def 3;
then A90: 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
A91: lc /. 1 = (u * v) * w by IDEAL_1:def 8;
A92: lc . 1 = lc /. 1 by A90, PARTFUN1:def 6;
then consider x, y, z being Element of the carrier of (Polynom-Ring R), p being Polynomial of R such that
A93: LCT . (lc . 1) = p and
p = (x * y) * z and
A94: (u * v) * w = p . ((len fm1) -' 1) and
A95: len p <= len fm1 and
y in F . (m + 1) by A73, A91;
A96: lc = <*(lc . 1)*> by A88, A89, FINSEQ_1:40;
then A97: Sum lc = p . ((len fm1) -' 1) by A91, A92, A94, RLVECT_1:44;
consider LC being LinearCombination of FM1 such that
A98: LC = LCT * lc and
len LC = len lc by A75;
LC = <*(LCT . ((u * v) * w))*> by A96, A91, A92, A98, FINSEQ_2:35;
then Sum LC = p by A91, A92, A93, 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 A95, A98, A97; :: thesis: verum

end;

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

A112: now :: thesis: len (sLCp + sLCe) <= len fm1

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 A106, 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 A110, 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 A101, A107, A103, A100, RLVECT_1:41
.= sLCp + sLCe by A108, A104, 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 A100, A111, A112; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

A113: 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 A114: 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 A115: lc = <*> the carrier of R ;
consider LC being LinearCombination of FM1 such that
A116: LC = LCT * lc and
A117: len lc = len LC by A75;
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 A116; :: thesis: ( p = Sum LC & p . ((len fm1) -' 1) = Sum lc & len p <= len fm1 )
LC = <*> the carrier of (Polynom-Ring R) by A114, A117;
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
.= Sum lc by A115, RLVECT_1:43 ; :: thesis: len p <= len fm1
thus len p <= len fm1 by POLYNOM4:3; :: thesis: verum

end;

for k being Nat holds S₆[k] from NAT_1:sch 2(A113, A84);
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 A83; :: thesis: verum

end;

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

A122: now :: thesis: not len (fm1 - sLC) = len fm1

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 A30;
then A123: (fm1 - sLC) . ((len fm1) -' 1) = (fm1 . ((len fm1) -' 1)) - (fm1 . ((len fm1) -' 1)) by A74, A119, POLYNOM3:27
.= 0. R by RLVECT_1:15 ;
(len fm1) - 1 >= 0 by A28;
then A124: ((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 A124, A123, ALGSEQ_1:10; :: thesis: verum

end;

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

A126: now :: thesis: not fm1 - sLC in FM1 -Ideal

reconsider sLC = sLC as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
assume A127: 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 A125, POLYNOM3:def 10;
then fm1 in FM1 -Ideal by A121, A127, IDEAL_1:def 1;
hence contradiction by A32, XBOOLE_0:def 5; :: thesis: verum

end;

len (- sLC) <= len fm1 by A120, POLYNOM4:8;
then len (fm1 - sLC) <= len fm1 by POLYNOM4:6;
then A128: len (fm1 - sLC) < len fm1 by A122, 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 A129: FM1 -Ideal c= I by IDEAL_1:44;
( f . (m + 1) in I & f9 = (f . (m + 1)) - sLC ) by A32, Th16, XBOOLE_0:def 5;
hence fm1 - sLC in I by A121, A129, IDEAL_1:15; :: thesis: verum

end;

then fm1 - sLC in I \ (FM1 -Ideal) by A126, XBOOLE_0:def 5;
hence contradiction by A128, A32, Th17; :: thesis: verum

end;

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