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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L)
for G being Subset of (Polynom-Ring n,L)
for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T holds
G \ {p} 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 associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L)
for G being Subset of (Polynom-Ring n,L)
for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T
let L be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for I being non empty add-closed left-ideal Subset of (Polynom-Ring n,L)
for G being Subset of (Polynom-Ring n,L)
for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T
let I be non empty add-closed left-ideal Subset of (Polynom-Ring n,L); :: thesis: for G being Subset of (Polynom-Ring n,L)
for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T
let G be Subset of (Polynom-Ring n,L); :: thesis: for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T
let p be Polynomial of n,L; :: thesis: for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T
let q be non-zero Polynomial of n,L; :: thesis: ( p in G & q in G & p <> q & HT q,T divides HT p,T & G is_Groebner_basis_of I,T implies G \ {p} is_Groebner_basis_of I,T )
assume that
A1: p in G and
A2: q in G and
A3: p <> q and
A4: HT q,T divides HT p,T ; :: thesis: ( not G is_Groebner_basis_of I,T or G \ {p} is_Groebner_basis_of I,T )
reconsider GG = G as non empty Subset of (Polynom-Ring n,L) by A1;
assume A5: G is_Groebner_basis_of I,T ; :: thesis: G \ {p} is_Groebner_basis_of I,T
set G9 = G \ {p};
A6: not q in {p} by A3, TARSKI:def 1;
then ( q <> 0_ n,L & q in G \ {p} ) by A2, POLYNOM7:def 2, XBOOLE_0:def 5;
then A7: HT q,T in { (HT u,T) where u is Polynomial of n,L : ( u in G \ {p} & u <> 0_ n,L ) } ;
GG c= GG -Ideal by IDEAL_1:def 15;
then A8: G c= I by A5, Def4;
for f being Polynomial of n,L st f in I holds
PolyRedRel G,T reduces f, 0_ n,L by A1, A5, Th24;
then for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt G,T by Th25;
then A9: for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T by A8, Th26;
for b being bag of n st b in HT I,T holds
ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b )

proof

let b be bag of n; :: thesis: ( b in HT I,T implies ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b ) )
assume b in HT I,T ; :: thesis: ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b )
then consider bb being bag of n such that
A10: bb in HT G,T and
A11: bb divides b by A9, Th27;
consider r being Polynomial of n,L such that
A12: bb = HT r,T and
A13: r in G and
A14: r <> 0_ n,L by A10;

now

per cases ( r = p or r <> p ) ;

case r = p ; :: thesis: ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b )

hence ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b ) by A4, A7, A11, A12, Lm8; :: thesis: verum

end;

case r <> p ; :: thesis: ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b )

then not r in {p} by TARSKI:def 1;
then r in G \ {p} by A13, XBOOLE_0:def 5;
then bb in { (HT u,T) where u is Polynomial of n,L : ( u in G \ {p} & u <> 0_ n,L ) } by A12, A14;
hence ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b ) by A11; :: thesis: verum

end;

end;

end;

hence ex b9 being bag of n st
( b9 in HT (G \ {p}),T & b9 divides b ) ; :: thesis: verum

end;

then A15: HT I,T c= multiples (HT (G \ {p}),T) by Th28;
G \ {p} c= G by XBOOLE_1:36;
then A16: G \ {p} c= I by A8, XBOOLE_1:1;
G \ {p} <> {} by A2, A6, XBOOLE_0:def 5;
hence G \ {p} is_Groebner_basis_of I,T by A16, A15, Th29; :: thesis: verum