let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let G be Subset of (Polynom-Ring (n,L)); :: thesis:
set R = PolyRedRel (G,T);
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:

now :: thesis:

let g1, g2 be Polynomial of n,L; :: thesis:

now :: thesis:

per cases ;

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

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

end;

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

hence S-Poly (g1,g2,T) has_a_normal_form_wrt PolyRedRel (G,T) by REWRITE1:46; :: thesis:

end;

end;

end;

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

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: