set cR = the carrier of R;

set PR = Polynom-Ring R;

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

set PR = Polynom-Ring R;

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

now :: thesis: Polynom-Ring R is Noetherian

hence
Polynom-Ring R is Noetherian
; :: thesis: verumassume
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_{1}[ set , set , set ] means ( c_{2} 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_{2} & B = I \ (A -Ideal) & ex r being Element of the carrier of (Polynom-Ring R) st

( r in minlen B & c_{3} = c_{2} \/ {r} ) ) );

A6: ( F . 0 = {(0. (Polynom-Ring R))} & ( for n being Nat holds S_{1}[n,F . n,F . (n + 1)] ) )
from RECDEF_1:sch 2(A2);

defpred S_{2}[ 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_{2}} & c_{2} in minlen B );

defpred S_{3}[ Nat] means F . R is non empty finite Subset of I;

_{3}[ 0 ]
by A6;

A13: for n being Nat holds S_{3}[n]
from NAT_1:sch 2(A12, A7);

A15: for x being Element of NAT holds S_{2}[x,f . x]
from FUNCT_2:sch 3(A14);

A16: for x being Nat holds S_{2}[x,f . x]

F . i c= F . j_{4}[ set , set ] means ex n being Element of NAT ex A being Polynomial of R st

( n = R & A = f . n & c_{2} = A . ((len A) -' 1) );

A30: for x being Element of NAT holds S_{4}[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_{5}[ 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_{2} = 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

ex d being object st

( d in the carrier of (Polynom-Ring R) & S_{5}[e,d] )

A73: for e being object st e in the carrier of R holds

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

( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

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;

.= fm1 + (sLC - sLC)

.= fm1 + (0_. R) by POLYNOM3:29

.= fm1 by POLYNOM3:28 ;

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

hence contradiction by A128, A32, Th17; :: thesis: verum

end;then consider I being Ideal of (Polynom-Ring R) such that

A1: not I is finitely_generated ;

defpred S

( A = c

( r in minlen B & c

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_{1}[n,x,y]

consider F being sequence of (bool the carrier of (Polynom-Ring R)) such that for x being Subset of the carrier of (Polynom-Ring R) ex y being Subset of the carrier of (Polynom-Ring R) st S

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_{1}[y,b_{3},b_{4}]

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_{1}[y,b_{2},b_{3}]

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

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

end;

suppose
x is not non empty finite Subset of I
; :: thesis: ex y being Subset of the carrier of (Polynom-Ring R) st S_{1}[y,b_{2},b_{3}]

end;

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_{1}[y,b_{2},b_{3}]

then reconsider x9 = x as non empty Subset of the carrier of (Polynom-Ring R) ;

set B = I \ (x9 -Ideal);

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_{1}[n,x,x9 \/ {r}]
by A5;

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

end;set B = I \ (x9 -Ideal);

now :: thesis: not I \ (x9 -Ideal) = {}

then reconsider B = I \ (x9 -Ideal) as non empty Subset of the carrier of (Polynom-Ring R) ;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 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

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

hence ex y being Subset of the carrier of (Polynom-Ring R) st S

A6: ( F . 0 = {(0. (Polynom-Ring R))} & ( for n being Nat holds S

defpred S

( A = F . n & B = I \ (A -Ideal) & n = R & F . (n + 1) = (F . n) \/ {c

defpred S

A7: now :: thesis: for n being Nat st S_{3}[n] holds

S_{3}[n + 1]

F . 0 c= I
S

let n be Nat; :: thesis: ( S_{3}[n] implies S_{3}[n + 1] )

assume S_{3}[n]
; :: thesis: S_{3}[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_{3}[n + 1]
by A11, XBOOLE_1:8; :: thesis: verum

end;assume S

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

proof

then A12:
S
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;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

A13: for n being Nat holds S

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

consider f being sequence of the carrier of (Polynom-Ring R) such that let x be Element of NAT ; :: thesis: ex y being Element of the carrier of (Polynom-Ring R) st S_{2}[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_{2}[x,y]
; :: thesis: verum

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

A15: for x being Element of NAT holds S

A16: for x being Nat holds S

proof

A17:
for i, j being Element of NAT st i <= j holds
let n be Nat; :: thesis: S_{2}[n,f . n]

n in NAT by ORDINAL1:def 12;

hence S_{2}[n,f . n]
by A15; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence S

F . i c= F . j

proof

A23:
for i being Element of NAT holds f . i <> 0. (Polynom-Ring R)
let i, j be Element of NAT ; :: thesis: ( i <= j implies F . i c= F . j )

defpred S_{4}[ 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_{4}[m] holds

S_{4}[m + 1]
_{4}[ 0 ]
;

A22: for m being Nat holds S_{4}[m]
from NAT_1:sch 2(A21, A19);

thus F . i c= F . j by A18, A22; :: thesis: verum

end;defpred S

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

S

proof

A21:
S
let m be Nat; :: thesis: ( S_{4}[m] implies S_{4}[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_{4}[m + 1]

hence S_{4}[m + 1]
by A20, XBOOLE_1:1; :: thesis: verum

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

hence S

A22: for m being Nat holds S

thus F . i c= F . j by A18, A22; :: thesis: verum

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

A28: now :: thesis: for i being Element of NAT

for fi being Polynomial of R st fi = f . i holds

(len fi) - 1 >= 0

defpred Sfor 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;(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

( n = R & A = f . n & c

A29: now :: thesis: for x being Element of NAT ex y being Element of the carrier of R st S_{4}[x,y]

consider a being sequence of the carrier of R such that let x be Element of NAT ; :: thesis: ex y being Element of the carrier of R st S_{4}[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_{4}[x,y]
; :: thesis: verum

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

A30: for x being Element of NAT holds S

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

( 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

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

A53:
for e being object st e in the carrier of R holds
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_{6}[ Nat] means for fk being Polynomial of R st fk = f . (i + R) holds

len fi <= len fk;

_{6}[ 0 ]
by A35;

A52: for k being Nat holds S_{6}[k]
from NAT_1:sch 2(A51, A38);

thus len fi <= len fj by A36, A37, A52; :: thesis: verum

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

len fi <= len fk;

A38: now :: thesis: for k being Nat st S_{6}[k] holds

S_{6}[k + 1]

A51:
SS

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

assume A39: S_{6}[k]
; :: thesis: S_{6}[k + 1]

_{6}[k + 1]
; :: thesis: verum

end;assume A39: S

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

len fi <= len fk1

hence
Slen 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;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

A52: for k being Nat holds S

thus len fi <= len fj by A36, A37, A52; :: thesis: verum

ex d being object st

( d in the carrier of (Polynom-Ring R) & S

proof

consider LCT being Function of the carrier of R, the carrier of (Polynom-Ring R) such that
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_{5}[e,d] ) )

assume e in the carrier of R ; :: thesis: ex d being object st

( d in the carrier of (Polynom-Ring R) & S_{5}[e,d] )

end;( d in the carrier of (Polynom-Ring R) & S

assume e in the carrier of R ; :: thesis: ex d being object st

( d in the carrier of (Polynom-Ring R) & S

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

end;

( 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_{5}[e,d] )

( 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

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_{5}[e,d] )
by A54, A69, A72, A70; :: thesis: verum

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

A73: for e being object st e in the carrier of R holds

S

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

for lc being LinearCombination of rng (a | (Segm (m + 1))) ex LC being LinearCombination of FM1 ex sLC being Polynomial of R st
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

LC = LC ;

hence ex LC being LinearCombination of FM1 st

( LC = LCT * lc & len lc = len LC ) by A77; :: thesis: verum

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

then reconsider LC = LCT * lc as LinearCombination of FM1 ;
let i be set ; :: according to IDEAL_1:def 8 :: thesis: ( not i in dom (LCT * lc) or ex b_{1}, b_{2} being Element of the carrier of (Polynom-Ring R) ex b_{3} being Element of FM1 st (LCT * lc) /. i = (b_{1} * b_{3}) * b_{2} )

assume A78: i in dom (LCT * lc) ; :: thesis: ex b_{1}, b_{2} being Element of the carrier of (Polynom-Ring R) ex b_{3} being Element of FM1 st (LCT * lc) /. i = (b_{1} * b_{3}) * b_{2}

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;assume A78: i in dom (LCT * lc) ; :: thesis: ex 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

LC = LC ;

hence ex LC being LinearCombination of FM1 st

( LC = LCT * lc & len lc = len LC ) by A77; :: thesis: verum

( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

proof

then consider LC being LinearCombination of FM1, sLC being Polynomial of R such that
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_{6}[ 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_{6}[k] holds

S_{6}[k + 1]
_{6}[ 0 ]
_{6}[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;( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 )

defpred S

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

S

proof

A113:
S
let k be Nat; :: thesis: ( S_{6}[k] implies S_{6}[k + 1] )

assume A85: S_{6}[k]
; :: thesis: S_{6}[k + 1]

thus S_{6}[k + 1]
:: thesis: verum

end;assume A85: S

thus S

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 )

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

end;

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 )

( 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;( LC = LCT * lc & sLC = Sum LC & sLC . ((len fm1) -' 1) = Sum lc & len sLC <= len fm1 ) by A85; :: thesis: verum

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 )

( 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

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

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

end;

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 )

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

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 )

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

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

dom LCT = the carrier of R
by FUNCT_2:def 1;end;

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

proof

for k being Nat holds S
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;( 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

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

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

A125: (fm1 - sLC) + sLC =
fm1 + (sLC + (- sLC))
by POLYNOM3:26
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;( 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

.= fm1 + (sLC - sLC)

.= fm1 + (0_. R) by POLYNOM3:29

.= fm1 by POLYNOM3:28 ;

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

len (- sLC) <= len fm1
by A120, POLYNOM4:8;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;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

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

then
fm1 - sLC in I \ (FM1 -Ideal)
by A126, XBOOLE_0:def 5;
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;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

hence contradiction by A128, A32, Th17; :: thesis: verum