let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let T be connected admissible TermOrder of n; :: thesis: for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

per cases
( I = {(0_ (n,L))} or I <> {(0_ (n,L))} )
;

end;

suppose A2:
I = {(0_ (n,L))}
; :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

set G = {(0_ (n,L))};

set R = PolyRedRel ({(0_ (n,L))},T);

take {(0_ (n,L))} ; :: thesis: {(0_ (n,L))} is_Groebner_basis_of I,T

{(0_ (n,L))} -Ideal = I by A2, IDEAL_1:44;

hence {(0_ (n,L))} is_Groebner_basis_of I,T by A9; :: thesis: verum

end;set R = PolyRedRel ({(0_ (n,L))},T);

take {(0_ (n,L))} ; :: thesis: {(0_ (n,L))} is_Groebner_basis_of I,T

now :: thesis: for a, b, c being object st [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) holds

b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

then A9:
PolyRedRel ({(0_ (n,L))},T) is locally-confluent
by REWRITE1:def 24;b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

let a, b, c be object ; :: thesis: ( [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) implies b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) )

assume that

A3: [a,b] in PolyRedRel ({(0_ (n,L))},T) and

[a,c] in PolyRedRel ({(0_ (n,L))},T) ; :: thesis: b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

consider p, q being object such that

A4: p in NonZero (Polynom-Ring (n,L)) and

A5: q in the carrier of (Polynom-Ring (n,L)) and

A6: [a,b] = [p,q] by A3, ZFMISC_1:def 2;

reconsider q = q as Polynomial of n,L by A5, POLYNOM1:def 11;

not p in {(0_ (n,L))} by A1, A4, XBOOLE_0:def 5;

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

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

p reduces_to q,{(0_ (n,L))},T by A3, A6, POLYRED:def 13;

then consider g being Polynomial of n,L such that

A7: g in {(0_ (n,L))} and

A8: p reduces_to q,g,T by POLYRED:def 7;

g = 0_ (n,L) by A7, TARSKI:def 1;

then p is_reducible_wrt 0_ (n,L),T by A8, POLYRED:def 8;

hence b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) by Lm3; :: thesis: verum

end;assume that

A3: [a,b] in PolyRedRel ({(0_ (n,L))},T) and

[a,c] in PolyRedRel ({(0_ (n,L))},T) ; :: thesis: b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)

consider p, q being object such that

A4: p in NonZero (Polynom-Ring (n,L)) and

A5: q in the carrier of (Polynom-Ring (n,L)) and

A6: [a,b] = [p,q] by A3, ZFMISC_1:def 2;

reconsider q = q as Polynomial of n,L by A5, POLYNOM1:def 11;

not p in {(0_ (n,L))} by A1, A4, XBOOLE_0:def 5;

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

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

p reduces_to q,{(0_ (n,L))},T by A3, A6, POLYRED:def 13;

then consider g being Polynomial of n,L such that

A7: g in {(0_ (n,L))} and

A8: p reduces_to q,g,T by POLYRED:def 7;

g = 0_ (n,L) by A7, TARSKI:def 1;

then p is_reducible_wrt 0_ (n,L),T by A8, POLYRED:def 8;

hence b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) by Lm3; :: thesis: verum

{(0_ (n,L))} -Ideal = I by A2, IDEAL_1:44;

hence {(0_ (n,L))} is_Groebner_basis_of I,T by A9; :: thesis: verum

suppose A10:
I <> {(0_ (n,L))}
; :: thesis: ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T

ex q being Element of I st q <> 0_ (n,L)

A14: q <> 0_ (n,L) ;

set R = RelStr(# (Bags n),(DivOrder n) #);

set hti = HT (I,T);

reconsider hti = HT (I,T) as Subset of RelStr(# (Bags n),(DivOrder n) #) ;

consider S being finite Subset of (Bags n) such that

A15: S is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) by Th34;

set M = { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } where s is Element of Bags n : s in S } ;

set s = the Element of S;

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

set hq = HT (q,T);

reconsider hq = HT (q,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

hq in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A14;

then ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S & b <= hq ) by A15, DICKSON:def 9;

then the Element of S in S ;

then { r where r is Polynomial of n,L : ( r in I & HT (r,T) = the Element of S & r <> 0_ (n,L) ) } in { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s9 & p <> 0_ (n,L) ) } where s9 is Element of Bags n : s9 in S } ;

then reconsider M = { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } where s is Element of Bags n : s in S } as non empty set ;

A16: for x, y being set st x in M & y in M & x <> y holds

x misses y

for x being set st x in M holds

x <> {}

A28: for x being set st x in M holds

ex y being object st G9 /\ x = {y} by A16, WELLORD2:18;

set xx = the Element of M;

A29: M is finite

set xx = the Element of M;

reconsider G9 = G9 as non empty set by A37;

set G = { x where x is Element of G9 : ex y being set st

( y in M & G9 /\ y = {x} ) } ;

( y in M & G9 /\ y = {x} ) } as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;

defpred S_{1}[ object , object ] means ex D1 being set st

( D1 = $1 & G9 /\ D1 = {$2} & $2 in G );

A43: for x being object st x in M holds

ex y being object st S_{1}[x,y]

A46: ( dom f = M & ( for x being object st x in M holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A43);

consider y being object such that

A55: G9 /\ the Element of M = {y} by A28;

y in G9 /\ the Element of M by A55, TARSKI:def 1;

then y in G9 by XBOOLE_0:def 4;

then y in G by A55;

then ( not G is empty & G is finite ) by A29, A46, A54, FINSET_1:8;

then reconsider G = G as non empty finite Subset of (Polynom-Ring (n,L)) ;

for b being bag of n st b in HT (I,T) holds

ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

take G ; :: thesis: G is_Groebner_basis_of I,T

hence G is_Groebner_basis_of I,T by A63, Th29; :: thesis: verum

end;proof

then consider q being Element of I such that
assume A11:
for q being Element of I holds not q <> 0_ (n,L)
; :: thesis: contradiction

end;A12: now :: thesis: for u being object st u in {(0_ (n,L))} holds

u in I

u in I

let u be object ; :: thesis: ( u in {(0_ (n,L))} implies u in I )

assume u in {(0_ (n,L))} ; :: thesis: u in I

then A13: u = 0_ (n,L) by TARSKI:def 1;

end;assume u in {(0_ (n,L))} ; :: thesis: u in I

then A13: u = 0_ (n,L) by TARSKI:def 1;

now :: thesis: u in I

hence
u in I
; :: thesis: verumassume
not u in I
; :: thesis: contradiction

then for v being object holds not v in I by A11, A13;

hence contradiction by XBOOLE_0:def 1; :: thesis: verum

end;then for v being object holds not v in I by A11, A13;

hence contradiction by XBOOLE_0:def 1; :: thesis: verum

now :: thesis: for u being object st u in I holds

u in {(0_ (n,L))}

hence
contradiction
by A10, A12, TARSKI:2; :: thesis: verumu in {(0_ (n,L))}

let u be object ; :: thesis: ( u in I implies u in {(0_ (n,L))} )

assume u in I ; :: thesis: u in {(0_ (n,L))}

then u = 0_ (n,L) by A11;

hence u in {(0_ (n,L))} by TARSKI:def 1; :: thesis: verum

end;assume u in I ; :: thesis: u in {(0_ (n,L))}

then u = 0_ (n,L) by A11;

hence u in {(0_ (n,L))} by TARSKI:def 1; :: thesis: verum

A14: q <> 0_ (n,L) ;

set R = RelStr(# (Bags n),(DivOrder n) #);

set hti = HT (I,T);

reconsider hti = HT (I,T) as Subset of RelStr(# (Bags n),(DivOrder n) #) ;

consider S being finite Subset of (Bags n) such that

A15: S is_Dickson-basis_of hti, RelStr(# (Bags n),(DivOrder n) #) by Th34;

set M = { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } where s is Element of Bags n : s in S } ;

set s = the Element of S;

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

set hq = HT (q,T);

reconsider hq = HT (q,T) as Element of RelStr(# (Bags n),(DivOrder n) #) ;

hq in { (HT (p,T)) where p is Polynomial of n,L : ( p in I & p <> 0_ (n,L) ) } by A14;

then ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in S & b <= hq ) by A15, DICKSON:def 9;

then the Element of S in S ;

then { r where r is Polynomial of n,L : ( r in I & HT (r,T) = the Element of S & r <> 0_ (n,L) ) } in { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s9 & p <> 0_ (n,L) ) } where s9 is Element of Bags n : s9 in S } ;

then reconsider M = { { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } where s is Element of Bags n : s in S } as non empty set ;

A16: for x, y being set st x in M & y in M & x <> y holds

x misses y

proof

A24:
S c= hti
by A15, DICKSON:def 9;
let x, y be set ; :: thesis: ( x in M & y in M & x <> y implies x misses y )

assume that

A17: x in M and

A18: y in M and

A19: x <> y ; :: thesis: x misses y

consider t being Element of Bags n such that

A20: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = t & p <> 0_ (n,L) ) } and

t in S by A18;

consider s being Element of Bags n such that

A21: x = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

s in S by A17;

reconsider x = x, y = y as set ;

end;assume that

A17: x in M and

A18: y in M and

A19: x <> y ; :: thesis: x misses y

consider t being Element of Bags n such that

A20: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = t & p <> 0_ (n,L) ) } and

t in S by A18;

consider s being Element of Bags n such that

A21: x = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

s in S by A17;

reconsider x = x, y = y as set ;

now :: thesis: not x /\ y <> {}

hence
x misses y
by XBOOLE_0:def 7; :: thesis: verumset u = the Element of x /\ y;

assume A22: x /\ y <> {} ; :: thesis: contradiction

then the Element of x /\ y in y by XBOOLE_0:def 4;

then A23: ex v being Polynomial of n,L st

( the Element of x /\ y = v & v in I & HT (v,T) = t & v <> 0_ (n,L) ) by A20;

the Element of x /\ y in x by A22, XBOOLE_0:def 4;

then ex r being Polynomial of n,L st

( the Element of x /\ y = r & r in I & HT (r,T) = s & r <> 0_ (n,L) ) by A21;

hence contradiction by A19, A21, A20, A23; :: thesis: verum

end;assume A22: x /\ y <> {} ; :: thesis: contradiction

then the Element of x /\ y in y by XBOOLE_0:def 4;

then A23: ex v being Polynomial of n,L st

( the Element of x /\ y = v & v in I & HT (v,T) = t & v <> 0_ (n,L) ) by A20;

the Element of x /\ y in x by A22, XBOOLE_0:def 4;

then ex r being Polynomial of n,L st

( the Element of x /\ y = r & r in I & HT (r,T) = s & r <> 0_ (n,L) ) by A21;

hence contradiction by A19, A21, A20, A23; :: thesis: verum

for x being set st x in M holds

x <> {}

proof

then consider G9 being set such that
let x be set ; :: thesis: ( x in M implies x <> {} )

assume x in M ; :: thesis: x <> {}

then consider s being Element of Bags n such that

A25: x = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

A26: s in S ;

s in hti by A24, A26;

then consider q being Polynomial of n,L such that

A27: ( s = HT (q,T) & q in I & q <> 0_ (n,L) ) ;

q in x by A25, A27;

hence x <> {} ; :: thesis: verum

end;assume x in M ; :: thesis: x <> {}

then consider s being Element of Bags n such that

A25: x = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

A26: s in S ;

s in hti by A24, A26;

then consider q being Polynomial of n,L such that

A27: ( s = HT (q,T) & q in I & q <> 0_ (n,L) ) ;

q in x by A25, A27;

hence x <> {} ; :: thesis: verum

A28: for x being set st x in M holds

ex y being object st G9 /\ x = {y} by A16, WELLORD2:18;

set xx = the Element of M;

A29: M is finite

proof

A37:
ex y being object st G9 /\ the Element of M = {y}
by A28;
defpred S_{1}[ object , object ] means $2 = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = $1 & p <> 0_ (n,L) ) } ;

A30: for x being object st x in S holds

ex y being object st S_{1}[x,y]
;

consider f being Function such that

A31: ( dom f = S & ( for x being object st x in S holds

S_{1}[x,f . x] ) )
from CLASSES1:sch 1(A30);

hence M is finite by A31, FINSET_1:8; :: thesis: verum

end;A30: for x being object st x in S holds

ex y being object st S

consider f being Function such that

A31: ( dom f = S & ( for x being object st x in S holds

S

A32: now :: thesis: for u being object st u in rng f holds

u in M

u in M

let u be object ; :: thesis: ( u in rng f implies u in M )

assume u in rng f ; :: thesis: u in M

then consider s being object such that

A33: s in dom f and

A34: u = f . s by FUNCT_1:def 3;

u = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } by A31, A33, A34;

hence u in M by A31, A33; :: thesis: verum

end;assume u in rng f ; :: thesis: u in M

then consider s being object such that

A33: s in dom f and

A34: u = f . s by FUNCT_1:def 3;

u = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } by A31, A33, A34;

hence u in M by A31, A33; :: thesis: verum

now :: thesis: for u being object st u in M holds

u in rng f

then
rng f = M
by A32, TARSKI:2;u in rng f

let u be object ; :: thesis: ( u in M implies u in rng f )

assume u in M ; :: thesis: u in rng f

then consider s being Element of Bags n such that

A35: u = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

A36: s in S ;

f . s in rng f by A31, A36, FUNCT_1:3;

hence u in rng f by A31, A35, A36; :: thesis: verum

end;assume u in M ; :: thesis: u in rng f

then consider s being Element of Bags n such that

A35: u = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

A36: s in S ;

f . s in rng f by A31, A36, FUNCT_1:3;

hence u in rng f by A31, A35, A36; :: thesis: verum

hence M is finite by A31, FINSET_1:8; :: thesis: verum

set xx = the Element of M;

reconsider G9 = G9 as non empty set by A37;

set G = { x where x is Element of G9 : ex y being set st

( y in M & G9 /\ y = {x} ) } ;

now :: thesis: for u being object st u in { x where x is Element of G9 : ex y being set st

( y in M & G9 /\ y = {x} ) } holds

u in the carrier of (Polynom-Ring (n,L))

then reconsider G = { x where x is Element of G9 : ex y being set st ( y in M & G9 /\ y = {x} ) } holds

u in the carrier of (Polynom-Ring (n,L))

let u be object ; :: thesis: ( u in { x where x is Element of G9 : ex y being set st

( y in M & G9 /\ y = {x} ) } implies u in the carrier of (Polynom-Ring (n,L)) )

assume u in { x where x is Element of G9 : ex y being set st

( y in M & G9 /\ y = {x} ) } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then consider x being Element of G9 such that

A38: u = x and

A39: ex y being set st

( y in M & G9 /\ y = {x} ) ;

consider y being set such that

A40: y in M and

A41: G9 /\ y = {x} by A39;

consider s being Element of Bags n such that

A42: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

s in S by A40;

x in G9 /\ y by A41, TARSKI:def 1;

then x in y by XBOOLE_0:def 4;

then ex q being Polynomial of n,L st

( x = q & q in I & HT (q,T) = s & q <> 0_ (n,L) ) by A42;

hence u in the carrier of (Polynom-Ring (n,L)) by A38; :: thesis: verum

end;( y in M & G9 /\ y = {x} ) } implies u in the carrier of (Polynom-Ring (n,L)) )

assume u in { x where x is Element of G9 : ex y being set st

( y in M & G9 /\ y = {x} ) } ; :: thesis: u in the carrier of (Polynom-Ring (n,L))

then consider x being Element of G9 such that

A38: u = x and

A39: ex y being set st

( y in M & G9 /\ y = {x} ) ;

consider y being set such that

A40: y in M and

A41: G9 /\ y = {x} by A39;

consider s being Element of Bags n such that

A42: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

s in S by A40;

x in G9 /\ y by A41, TARSKI:def 1;

then x in y by XBOOLE_0:def 4;

then ex q being Polynomial of n,L st

( x = q & q in I & HT (q,T) = s & q <> 0_ (n,L) ) by A42;

hence u in the carrier of (Polynom-Ring (n,L)) by A38; :: thesis: verum

( y in M & G9 /\ y = {x} ) } as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;

defpred S

( D1 = $1 & G9 /\ D1 = {$2} & $2 in G );

A43: for x being object st x in M holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in M implies ex y being object st S_{1}[x,y] )

assume A44: x in M ; :: thesis: ex y being object st S_{1}[x,y]

reconsider xx = x as set by TARSKI:1;

consider y being object such that

A45: G9 /\ xx = {y} by A28, A44;

y in G9 /\ xx by A45, TARSKI:def 1;

then reconsider y = y as Element of G9 by XBOOLE_0:def 4;

y in G by A44, A45;

hence ex y being object st S_{1}[x,y]
by A45; :: thesis: verum

end;assume A44: x in M ; :: thesis: ex y being object st S

reconsider xx = x as set by TARSKI:1;

consider y being object such that

A45: G9 /\ xx = {y} by A28, A44;

y in G9 /\ xx by A45, TARSKI:def 1;

then reconsider y = y as Element of G9 by XBOOLE_0:def 4;

y in G by A44, A45;

hence ex y being object st S

A46: ( dom f = M & ( for x being object st x in M holds

S

A47: now :: thesis: for u being object st u in G holds

u in rng f

u in rng f

let u be object ; :: thesis: ( u in G implies u in rng f )

assume u in G ; :: thesis: u in rng f

then consider x being Element of G9 such that

A48: u = x and

A49: ex y being set st

( y in M & G9 /\ y = {x} ) ;

consider y being set such that

A50: y in M and

A51: G9 /\ y = {x} by A49;

S_{1}[y,f . y]
by A46, A50;

then G9 /\ y = {(f . y)} ;

then A52: x in {(f . y)} by A51, TARSKI:def 1;

f . y in rng f by A46, A50, FUNCT_1:3;

hence u in rng f by A48, A52, TARSKI:def 1; :: thesis: verum

end;assume u in G ; :: thesis: u in rng f

then consider x being Element of G9 such that

A48: u = x and

A49: ex y being set st

( y in M & G9 /\ y = {x} ) ;

consider y being set such that

A50: y in M and

A51: G9 /\ y = {x} by A49;

S

then G9 /\ y = {(f . y)} ;

then A52: x in {(f . y)} by A51, TARSKI:def 1;

f . y in rng f by A46, A50, FUNCT_1:3;

hence u in rng f by A48, A52, TARSKI:def 1; :: thesis: verum

now :: thesis: for u being object st u in rng f holds

u in G

then A54:
rng f = G
by A47, TARSKI:2;u in G

let u be object ; :: thesis: ( u in rng f implies u in G )

assume u in rng f ; :: thesis: u in G

then consider s being object such that

A53: ( s in dom f & u = f . s ) by FUNCT_1:def 3;

S_{1}[s,f . s]
by A46, A53;

hence u in G by A53; :: thesis: verum

end;assume u in rng f ; :: thesis: u in G

then consider s being object such that

A53: ( s in dom f & u = f . s ) by FUNCT_1:def 3;

S

hence u in G by A53; :: thesis: verum

consider y being object such that

A55: G9 /\ the Element of M = {y} by A28;

y in G9 /\ the Element of M by A55, TARSKI:def 1;

then y in G9 by XBOOLE_0:def 4;

then y in G by A55;

then ( not G is empty & G is finite ) by A29, A46, A54, FINSET_1:8;

then reconsider G = G as non empty finite Subset of (Polynom-Ring (n,L)) ;

for b being bag of n st b in HT (I,T) holds

ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

proof

then A63:
HT (I,T) c= multiples (HT (G,T))
by Th28;
let b be bag of n; :: thesis: ( b in HT (I,T) implies ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b ) )

reconsider bb = b as Element of RelStr(# (Bags n),(DivOrder n) #) by PRE_POLY:def 12;

assume b in HT (I,T) ; :: thesis: ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

then consider bb9 being Element of RelStr(# (Bags n),(DivOrder n) #) such that

A56: bb9 in S and

A57: bb9 <= bb by A15, DICKSON:def 9;

set N = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } ;

A58: { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } in M by A56;

then consider y being object such that

A59: G9 /\ { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } = {y} by A28;

reconsider b9 = bb9 as bag of n ;

take b9 ; :: thesis: ( b9 in HT (G,T) & b9 divides b )

A60: [bb9,bb] in DivOrder n by A57, ORDERS_2:def 5;

A61: y in G9 /\ { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } by A59, TARSKI:def 1;

then reconsider y = y as Element of G9 by XBOOLE_0:def 4;

y in { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } by A61, XBOOLE_0:def 4;

then A62: ex r being Polynomial of n,L st

( y = r & r in I & HT (r,T) = bb9 & r <> 0_ (n,L) ) ;

y in G by A58, A59;

hence ( b9 in HT (G,T) & b9 divides b ) by A60, A62, Def5; :: thesis: verum

end;( b9 in HT (G,T) & b9 divides b ) )

reconsider bb = b as Element of RelStr(# (Bags n),(DivOrder n) #) by PRE_POLY:def 12;

assume b in HT (I,T) ; :: thesis: ex b9 being bag of n st

( b9 in HT (G,T) & b9 divides b )

then consider bb9 being Element of RelStr(# (Bags n),(DivOrder n) #) such that

A56: bb9 in S and

A57: bb9 <= bb by A15, DICKSON:def 9;

set N = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } ;

A58: { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } in M by A56;

then consider y being object such that

A59: G9 /\ { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } = {y} by A28;

reconsider b9 = bb9 as bag of n ;

take b9 ; :: thesis: ( b9 in HT (G,T) & b9 divides b )

A60: [bb9,bb] in DivOrder n by A57, ORDERS_2:def 5;

A61: y in G9 /\ { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } by A59, TARSKI:def 1;

then reconsider y = y as Element of G9 by XBOOLE_0:def 4;

y in { p where p is Polynomial of n,L : ( p in I & HT (p,T) = bb9 & p <> 0_ (n,L) ) } by A61, XBOOLE_0:def 4;

then A62: ex r being Polynomial of n,L st

( y = r & r in I & HT (r,T) = bb9 & r <> 0_ (n,L) ) ;

y in G by A58, A59;

hence ( b9 in HT (G,T) & b9 divides b ) by A60, A62, Def5; :: thesis: verum

take G ; :: thesis: G is_Groebner_basis_of I,T

now :: thesis: for u being object st u in G holds

u in I

then
G c= I
;u in I

let u be object ; :: thesis: ( u in G implies u in I )

assume u in G ; :: thesis: u in I

then consider x being Element of G9 such that

A64: u = x and

A65: ex y being set st

( y in M & G9 /\ y = {x} ) ;

consider y being set such that

A66: y in M and

A67: G9 /\ y = {x} by A65;

consider s being Element of Bags n such that

A68: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

s in S by A66;

x in G9 /\ y by A67, TARSKI:def 1;

then x in y by XBOOLE_0:def 4;

then ex q being Polynomial of n,L st

( x = q & q in I & HT (q,T) = s & q <> 0_ (n,L) ) by A68;

hence u in I by A64; :: thesis: verum

end;assume u in G ; :: thesis: u in I

then consider x being Element of G9 such that

A64: u = x and

A65: ex y being set st

( y in M & G9 /\ y = {x} ) ;

consider y being set such that

A66: y in M and

A67: G9 /\ y = {x} by A65;

consider s being Element of Bags n such that

A68: y = { p where p is Polynomial of n,L : ( p in I & HT (p,T) = s & p <> 0_ (n,L) ) } and

s in S by A66;

x in G9 /\ y by A67, TARSKI:def 1;

then x in y by XBOOLE_0:def 4;

then ex q being Polynomial of n,L st

( x = q & q in I & HT (q,T) = s & q <> 0_ (n,L) ) by A68;

hence u in I by A64; :: thesis: verum

hence G is_Groebner_basis_of I,T by A63, Th29; :: thesis: verum