let n be Element of NAT ; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non degenerated non trivial 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:
assume A1: not 0_ (n,L) in G ; :: thesis:
assume A2: for g1, g2 being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint holds
PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 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)

proof

let g1, g2 be Polynomial of n,L; :: thesis:
assume that
A3: g1 in G and
A4: g2 in G ; :: thesis:

now :: thesis:

per cases ;

case A5: HT (g1,T), HT (g2,T) are_disjoint ; :: thesis:

now :: thesis:

let u be object ; :: thesis:
assume A6: u in {g1,g2} ; :: thesis:

now :: thesis:

per cases by A6, TARSKI:def 2;

case u = g1 ; :: thesis:

hence u in G by A3; :: thesis:

end;

case u = g2 ; :: thesis:

hence u in G by A4; :: thesis:

end;

end;

end;

hence u in G ; :: thesis:

end;

then A7: {g1,g2} c= G ;
PolyRedRel ({g1,g2},T) reduces S-Poly (g1,g2,T), 0_ (n,L) by A5, Th56;
hence PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by A7, GROEB_1:4, REWRITE1:22; :: thesis:

end;

case not HT (g1,T), HT (g2,T) are_disjoint ; :: thesis:

hence PolyRedRel (G,T) reduces S-Poly (g1,g2,T), 0_ (n,L) by A2, A3, A4; :: thesis:

end;

end;

end;

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

end;

then G is_Groebner_basis_wrt T by A1, GROEB_2:25;
hence for g1, g2, h being Polynomial of n,L st g1 in G & g2 in G & not HT (g1,T), HT (g2,T) are_disjoint & h is_a_normal_form_of S-Poly (g1,g2,T), PolyRedRel (G,T) holds
h = 0_ (n,L) by GROEB_2:23; :: thesis: