let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let I be non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)); :: thesis:
A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

suppose A2: I = {(0_ (n,L))} ; :: thesis:

set G = {(0_ (n,L))};
set R = PolyRedRel ({(0_ (n,L))},T);
take {(0_ (n,L))} ; :: thesis:

now :: thesis:

let a, b, c be object ; :: thesis:
assume that
A3: [a,b] in PolyRedRel ({(0_ (n,L))},T) and
[a,c] in PolyRedRel ({(0_ (n,L))},T) ; :: thesis:
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:

end;

then A9: PolyRedRel ({(0_ (n,L))},T) is locally-confluent by REWRITE1:def 24;
{(0_ (n,L))} -Ideal = I by A2, IDEAL_1:44;
hence {(0_ (n,L))} is_Groebner_basis_of I,T by A9; :: thesis:

end;

suppose A10: I <> {(0_ (n,L))} ; :: thesis:

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

proof

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

A12: now :: thesis:

let u be object ; :: thesis:
assume u in {(0_ (n,L))} ; :: thesis:
then A13: u = 0_ (n,L) by TARSKI:def 1;

now :: thesis:

assume not u in I ; :: thesis:
then for v being object holds not v in I by A11, A13;
hence contradiction by XBOOLE_0:def 1; :: thesis:

end;

hence u in I ; :: thesis:

end;

now :: thesis:

let u be object ; :: thesis:
assume u in I ; :: thesis:
then u = 0_ (n,L) by A11;
hence u in {(0_ (n,L))} by TARSKI:def 1; :: thesis:

end;

hence contradiction by A10, A12, TARSKI:2; :: thesis:

end;

then consider q being Element of I such that
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

let x, y be set ; :: thesis:
assume that
A17: x in M and
A18: y in M and
A19: x <> y ; :: thesis:
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:

set u = the Element of x /\ y;
assume A22: x /\ y <> {} ; :: thesis:
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:

end;

hence x misses y by XBOOLE_0:def 7; :: thesis:

end;

A24: S c= hti by A15, DICKSON:def 9;
for x being set st x in M holds
x <> {}

proof

let x be set ; :: thesis:
assume x in M ; :: thesis:
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:

end;

then consider G9 being set such that
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

defpred S₁[ 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₁[x,y] ;
consider f being Function such that
A31: ( dom f = S & ( for x being object st x in S holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A30);

A32: now :: thesis:

let u be object ; :: thesis:
assume u in rng f ; :: thesis:
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:

end;

now :: thesis:

let u be object ; :: thesis:
assume u in M ; :: thesis:
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:

end;

then rng f = M by A32, TARSKI:2;
hence M is finite by A31, FINSET_1:8; :: thesis:

end;

A37: ex y being object st G9 /\ the Element of M = {y} by A28;
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:

let u be object ; :: thesis:
assume u in { x where x is Element of G9 : ex y being set st
( y in M & G9 /\ y = {x} ) } ; :: thesis:
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:

end;

then reconsider G = { x where x is Element of G9 : ex y being set st
( y in M & G9 /\ y = {x} ) } as Subset of (Polynom-Ring (n,L)) by TARSKI:def 3;
defpred S₁[ 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₁[x,y]

proof

let x be object ; :: thesis:
assume A44: x in M ; :: thesis:
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₁[x,y] by A45; :: thesis:

end;

consider f being Function such that
A46: ( dom f = M & ( for x being object st x in M holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A43);

A47: now :: thesis:

let u be object ; :: thesis:
assume u in G ; :: thesis:
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₁[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:

end;

now :: thesis:

let u be object ; :: thesis:
assume u in rng f ; :: thesis:
then consider s being object such that
A53: ( s in dom f & u = f . s ) by FUNCT_1:def 3;
S₁[s,f . s] by A46, A53;
hence u in G by A53; :: thesis:

end;

then A54: rng f = G by A47, TARSKI:2;
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

let b be bag of n; :: thesis:
reconsider bb = b as Element of RelStr(# (Bags n),(DivOrder n) #) by PRE_POLY:def 12;
assume b in HT (I,T) ; :: thesis:
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:
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:

end;

then A63: HT (I,T) c= multiples (HT (G,T)) by Th28;
take G ; :: thesis:

now :: thesis:

let u be object ; :: thesis:
assume u in G ; :: thesis:
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:

end;

then G c= I ;
hence G is_Groebner_basis_of I,T by A63, Th29; :: thesis:

end;