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))
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 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))
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 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))
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 1, 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 14;
then A8: G c= I by A5;
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 :: thesis: ( ( r = p & ex b9 being bag of n st
( b9 in HT ((G \ {p}),T) & b9 divides b ) ) or ( r <> p & ex b9 being bag of n st
( b9 in HT ((G \ {p}),T) & b9 divides b ) ) )

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;
G \ {p} <> {} by A2, A6, XBOOLE_0:def 5;
hence G \ {p} is_Groebner_basis_of I,T by A16, A15, Th29; :: thesis: verum