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 G is_Groebner_basis_wrt T holds
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
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 G is_Groebner_basis_wrt T holds
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
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 G is_Groebner_basis_wrt T holds
for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
let G be Subset of (Polynom-Ring (n,L)); :: thesis: ( G is_Groebner_basis_wrt T implies for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) )
assume A1: G is_Groebner_basis_wrt T ; :: thesis: for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)
set R = PolyRedRel (G,T);
A2: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;

per cases ( G = {} or G <> {} ) ;

suppose G = {} ; :: thesis: for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)

hence for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ; :: thesis: verum

end;

suppose G <> {} ; :: thesis: for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)

then reconsider G = G as non empty Subset of (Polynom-Ring (n,L)) ;
A3: PolyRedRel (G,T) is locally-confluent by A1, GROEB_1:def 3;

now :: thesis: for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L)

A4: now :: thesis: 0_ (n,L) is_a_normal_form_wrt PolyRedRel (G,T)

assume not 0_ (n,L) is_a_normal_form_wrt PolyRedRel (G,T) ; :: thesis: contradiction
then consider b being object such that
A5: [(0_ (n,L)),b] in PolyRedRel (G,T) by REWRITE1:def 5;
consider f1, f2 being object such that
A6: f1 in NonZero (Polynom-Ring (n,L)) and
f2 in the carrier of (Polynom-Ring (n,L)) and
A7: [(0_ (n,L)),b] = [f1,f2] by A5, ZFMISC_1:def 2;
A8: f1 = 0_ (n,L) by A7, XTUPLE_0:1;
not f1 in {(0_ (n,L))} by A2, A6, XBOOLE_0:def 5;
hence contradiction by A8, TARSKI:def 1; :: thesis: verum

end;

let g1, g2, h be Polynomial of n,L; :: thesis: ( g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) implies h = 0_ (n,L) )
assume that
A9: ( g1 in G & g2 in G ) and
A10: h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) ; :: thesis: h = 0_ (n,L)
S-Poly (g1,g2,T) in G -Ideal by A9, Th18;
then PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by A3, GROEB_1:15;
then A11: S-Poly (g1,g2,T), 0_ (n,L) are_convertible_wrt PolyRedRel (G,T) by REWRITE1:25;
PolyRedRel (G,T) reduces S-Poly (g1,g2,T),h by A10, REWRITE1:def 6;
then h, S-Poly (g1,g2,T) are_convertible_wrt PolyRedRel (G,T) by REWRITE1:25;
then A12: h, 0_ (n,L) are_convertible_wrt PolyRedRel (G,T) by A11, REWRITE1:30;
h is_a_normal_form_wrt PolyRedRel (G,T) by A10, REWRITE1:def 6;
hence h = 0_ (n,L) by A3, A4, A12, REWRITE1:def 19; :: thesis: verum

end;

hence for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) ; :: thesis: verum

end;

end;