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 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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 associative commutative well-unital distributive Abelian add-associative right_zeroed 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;
X: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;

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) ;
PolyRedRel G,T is locally-confluent by A1, GROEB_1:def 3;
then A2: PolyRedRel G,T is with_UN_property ;

now

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 A3: ( g1 in G & g2 in G & h is_a_normal_form_of S-Poly g1,g2,T, PolyRedRel G,T ) ; :: thesis: h = 0_ n,L
then S-Poly g1,g2,T in G -Ideal by Th22;
then A4: PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L by A2, GROEB_1:15;

A5: now

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

end;

A9: ( h is_a_normal_form_wrt PolyRedRel G,T & PolyRedRel G,T reduces S-Poly g1,g2,T,h ) by A3, REWRITE1:def 6;
then ( S-Poly g1,g2,T, 0_ n,L are_convertible_wrt PolyRedRel G,T & h, S-Poly g1,g2,T are_convertible_wrt PolyRedRel G,T ) by A4, REWRITE1:26;
then h, 0_ n,L are_convertible_wrt PolyRedRel G,T by REWRITE1:31;
hence h = 0_ n,L by A2, A5, A9, 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;