theorem
for
n being
Element of
NAT 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 ( 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)