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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 27;
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, Def4;
A5: PolyRedRel G,T is locally-confluent by A3, Def4;
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) ;

A7: now

per cases ;

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

now

per cases ;

case G = {} ; :: thesis:

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

end;

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

A10: now

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

now

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

end;

hence u in G by A9; :: thesis:

end;

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

now

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

end;

then G = {(0_ n,L)} by A10, TARSKI:2;
hence G9 -Ideal = I by A1, A4, A13, 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) ;
A15: 0. (Polynom-Ring n,L) = 0_ n,L by POLYNOM1:def 27;

A16: now

let u be set ; :: 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 A15, Lm9;
hence u in G9 -Ideal by IDEAL_1:60; :: thesis:

end;

now

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

end;

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

end;

end;

end;

A18: now

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;

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

proof

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

end;

PolyRedRel (G \ {(0_ n,L)}),T c= PolyRedRel G,T by Th4, XBOOLE_1:36;
then for u being set 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, A19, TARSKI:2;
then G9 is_Groebner_basis_of I,T by A7, Def4;
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 A18; :: thesis: