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 ( 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 ) holds
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
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 ( 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 ) holds
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
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 ( 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 ) holds
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
let G be Subset of (Polynom-Ring n,L); :: 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 ) implies 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 )
assume A1: 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: 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
set R = PolyRedRel G,T;

now

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 A2: ( g1 in G & g2 in G ) ; :: thesis: PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L

now

per cases ( S-Poly g1,g2,T in field (PolyRedRel G,T) or not S-Poly g1,g2,T in field (PolyRedRel G,T) ) ;

case S-Poly g1,g2,T in field (PolyRedRel G,T) ; :: thesis: S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T

hence S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T by REWRITE1:def 14; :: thesis: verum

end;

case not S-Poly g1,g2,T in field (PolyRedRel G,T) ; :: thesis: S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T

hence S-Poly g1,g2,T has_a_normal_form_wrt PolyRedRel G,T by REWRITE1:47; :: thesis: verum

end;

end;

end;

then consider q being set such that
A3: q is_a_normal_form_of S-Poly g1,g2,T, PolyRedRel G,T by REWRITE1:def 11;
( q is_a_normal_form_wrt PolyRedRel G,T & PolyRedRel G,T reduces S-Poly g1,g2,T,q ) by A3, REWRITE1:def 6;
then reconsider q = q as Polynomial of n,L by Lm1;
q = 0_ n,L by A1, A2, A3;
hence PolyRedRel G,T reduces S-Poly g1,g2,T, 0_ n,L by A3, REWRITE1:def 6; :: thesis: verum

end;

hence 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 ; :: thesis: verum