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:
assume A1: I <> {(0_ (n,L))} ; :: thesis:
A2: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
consider G being finite Subset of (Polynom-Ring (n,L)) such that
A3: G is_Groebner_basis_of I,T by Th35;
set R = PolyRedRel (G,T);
A4: G -Ideal = I by A3;
A5: PolyRedRel (G,T) is locally-confluent by A3;
set G9 = G \ {(0_ (n,L))};
set R9 = PolyRedRel ((G \ {(0_ (n,L))}),T);
reconsider G9 = G \ {(0_ (n,L))} as finite Subset of (Polynom-Ring (n,L)) ;

A6: now :: thesis:

per cases ;

case A7: G9 = {} ; :: thesis:

now :: thesis:

per cases ;

case G = {} ; :: thesis:

hence G9 -Ideal = I by A3; :: thesis:

end;

case A8: G <> {} ; :: thesis:

A9: now :: thesis:

let u be object ; :: thesis:
assume u in {(0_ (n,L))} ; :: thesis:
then A10: u = 0_ (n,L) by TARSKI:def 1;
A11: G c= {(0_ (n,L))} by A7, XBOOLE_1:37;

now :: thesis:

assume not u in G ; :: thesis:
then for v being object holds not v in G by A10, A11, TARSKI:def 1;
hence G = {} by XBOOLE_0:def 1; :: thesis:

end;

hence u in G by A8; :: thesis:

end;

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

now :: thesis:

let u be object ; :: thesis:
assume A13: u in G ; :: thesis:
G c= {(0_ (n,L))} by A7, XBOOLE_1:37;
hence u in {(0_ (n,L))} by A13; :: thesis:

end;

then G = {(0_ (n,L))} by A9, TARSKI:2;
hence G9 -Ideal = I by A1, A4, A12, IDEAL_1:44; :: thesis:

end;

end;

end;

hence G9 -Ideal = I ; :: thesis:

end;

case G9 <> {} ; :: thesis:

then reconsider GG = G, GG9 = G9 as non empty Subset of (Polynom-Ring (n,L)) ;
A14: 0. (Polynom-Ring (n,L)) = 0_ (n,L) by POLYNOM1:def 11;

A15: now :: thesis:

let u be object ; :: thesis:
assume u in G -Ideal ; :: thesis:
then ex f being LinearCombination of GG st u = Sum f by IDEAL_1:60;
then ex g being LinearCombination of GG9 st u = Sum g by A14, Lm9;
hence u in G9 -Ideal by IDEAL_1:60; :: thesis:

end;

now :: thesis:

let u be object ; :: thesis:
A16: GG9 -Ideal c= GG -Ideal by IDEAL_1:57, XBOOLE_1:36;
assume u in G9 -Ideal ; :: thesis:
hence u in G -Ideal by A16; :: thesis:

end;

hence G9 -Ideal = I by A4, A15, TARSKI:2; :: thesis:

end;

end;

end;

A17: now :: thesis:

assume 0_ (n,L) in G9 ; :: thesis:
then not 0_ (n,L) in {(0_ (n,L))} by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1; :: thesis:

end;

A18: for u being object st u in PolyRedRel (G,T) holds
u in PolyRedRel ((G \ {(0_ (n,L))}),T)

proof

let u be object ; :: thesis:
assume A19: u in PolyRedRel (G,T) ; :: thesis:
then consider p, q being object such that
A20: p in NonZero (Polynom-Ring (n,L)) and
A21: q in the carrier of (Polynom-Ring (n,L)) and
A22: u = [p,q] by ZFMISC_1:def 2;
reconsider q = q as Polynomial of n,L by A21, POLYNOM1:def 11;
not p in {(0_ (n,L))} by A2, A20, 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 A20, POLYNOM1:def 11, POLYNOM7:def 1;
p reduces_to q,G,T by A19, A22, POLYRED:def 13;
then consider f being Polynomial of n,L such that
A23: f in G and
A24: p reduces_to q,f,T by POLYRED:def 7;
ex b being bag of n st p reduces_to q,f,b,T by A24, POLYRED:def 6;
then f <> 0_ (n,L) by POLYRED:def 5;
then not f in {(0_ (n,L))} by TARSKI:def 1;
then f in G9 by A23, XBOOLE_0:def 5;
then p reduces_to q,G9,T by A24, POLYRED:def 7;
hence u in PolyRedRel ((G \ {(0_ (n,L))}),T) by A22, POLYRED:def 13; :: thesis:

end;

PolyRedRel ((G \ {(0_ (n,L))}),T) c= PolyRedRel (G,T) by Th4, XBOOLE_1:36;
then for u being object st u in PolyRedRel ((G \ {(0_ (n,L))}),T) holds
u in PolyRedRel (G,T) ;
then PolyRedRel ((G \ {(0_ (n,L))}),T) is locally-confluent by A5, A18, TARSKI:2;
then G9 is_Groebner_basis_of I,T by A6;
hence ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & not 0_ (n,L) in G ) by A17; :: thesis: