now

consider j being Element of { i where i is Element of NAT : i < 0 } ;
assume { i where i is Element of NAT : i < 0 } <> {} ; :: thesis: contradiction
then j in { i where i is Element of NAT : i < 0 } ;
then ex i being Element of NAT st
( i = j & i < 0 ) ;
hence contradiction by NAT_1:2; :: thesis: verum

end;

then reconsider n = {} as Element of NAT ;
let T be connected admissible TermOrder of {} ; :: 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 {} ,L)
for P being non empty Subset of (Polynom-Ring {} ,L) st P c= I & P <> {(0_ {} ,L)} holds
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 {} ,L)
for P being non empty Subset of (Polynom-Ring {} ,L) st P c= I & P <> {(0_ {} ,L)} holds
P is_Groebner_basis_of I,T
let I be non empty add-closed left-ideal Subset of (Polynom-Ring {} ,L); :: thesis: for P being non empty Subset of (Polynom-Ring {} ,L) st P c= I & P <> {(0_ {} ,L)} holds
P is_Groebner_basis_of I,T
let P be non empty Subset of (Polynom-Ring {} ,L); :: thesis: ( P c= I & P <> {(0_ {} ,L)} implies P is_Groebner_basis_of I,T )
assume that
A1: P c= I and
A2: P <> {(0_ {} ,L)} ; :: thesis: P is_Groebner_basis_of I,T
reconsider T = T as connected admissible TermOrder of n ;
reconsider P = P as non empty Subset of (Polynom-Ring n,L) ;
reconsider I = I as non empty add-closed left-ideal Subset of (Polynom-Ring n,L) ;
A3: ex q being Element of P st q <> 0_ n,L

proof

assume A4: for q being Element of P holds not q <> 0_ n,L ; :: thesis: contradiction

A5: now

let u be set ; :: thesis: ( u in {(0_ n,L)} implies u in P )
assume u in {(0_ n,L)} ; :: thesis: u in P
then A6: u = 0_ n,L by TARSKI:def 1;

now

assume not u in P ; :: thesis: contradiction
then for v being set holds not v in P by A4, A6;
hence contradiction by XBOOLE_0:def 1; :: thesis: verum

end;

hence u in P ; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in P implies u in {(0_ n,L)} )
assume u in P ; :: thesis: u in {(0_ n,L)}
then u = 0_ n,L by A4;
hence u in {(0_ n,L)} by TARSKI:def 1; :: thesis: verum

end;

hence contradiction by A2, A5, TARSKI:2; :: thesis: verum

end;

now

consider p being Element of P such that
A7: p <> 0_ n,L by A3;
reconsider p = p as Polynomial of n,L by POLYNOM1:def 27;
reconsider p = p as non-zero Polynomial of n,L by A7, POLYNOM7:def 2;
let f be non-zero Polynomial of n,L; :: thesis: ( f in I implies f is_reducible_wrt P,T )
assume f in I ; :: thesis: f is_reducible_wrt P,T
f <> 0_ n,L by POLYNOM7:def 2;
then Support f <> {} by POLYNOM7:1;
then HT f,T in Support f by TERMORD:def 6;
then ( HT p,T = EmptyBag n & EmptyBag n in Support f ) by POLYNOM7:3;
then f is_reducible_wrt p,T by POLYRED:36;
then consider g being Polynomial of n,L such that
A8: f reduces_to g,p,T by POLYRED:def 8;
f reduces_to g,P,T by A8, POLYRED:def 7;
hence f is_reducible_wrt P,T by POLYRED:def 9; :: thesis: verum

end;

then for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt P,T by A1, Th26;
then for b being bag of n st b in HT I,T holds
ex b9 being bag of n st
( b9 in HT P,T & b9 divides b ) by Th27;
then HT I,T c= multiples (HT P,T) by Th28;
hence P is_Groebner_basis_of I,T by A1, Th29; :: thesis: verum