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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt T

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) implies G is_Groebner_basis_wrt T )

assume that

A1: not 0_ (n,L) in G and

A2: for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ; :: thesis: G is_Groebner_basis_wrt T

for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr

for G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt 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 G being Subset of (Polynom-Ring (n,L)) st not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) holds

G is_Groebner_basis_wrt T

let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( not 0_ (n,L) in G & ( for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ) implies G is_Groebner_basis_wrt T )

assume that

A1: not 0_ (n,L) in G and

A2: for g being Polynomial of n,L st g in G holds

g is Monomial of n,L ; :: thesis: G is_Groebner_basis_wrt T

now :: thesis: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G holds

PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

hence
G is_Groebner_basis_wrt T
by A1, Th25; :: thesis: verumPolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

let g1, g2 be Polynomial of n,L; :: thesis: ( g1 in G & g2 in G implies PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) )

assume ( g1 in G & g2 in G ) ; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

then ( g1 is Monomial of n,L & g2 is Monomial of n,L ) by A2;

then S-Poly (g1,g2,T) = 0_ (n,L) by Th19;

hence PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by REWRITE1:12; :: thesis: verum

end;assume ( g1 in G & g2 in G ) ; :: thesis: PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L)

then ( g1 is Monomial of n,L & g2 is Monomial of n,L ) by A2;

then S-Poly (g1,g2,T) = 0_ (n,L) by Th19;

hence PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by REWRITE1:12; :: thesis: verum