let n be Element of NAT ; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T

let T be connected admissible TermOrder of n; :: thesis:
let L be non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T
set I = {(0_ (n,L))};
set G = {(0_ (n,L))};
set R = PolyRedRel ({(0_ (n,L))},T);
A1: 0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
now :: thesis: for a, b, c being object st [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) holds
b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)
let a, b, c be object ; :: thesis: ( [a,b] in PolyRedRel ({(0_ (n,L))},T) & [a,c] in PolyRedRel ({(0_ (n,L))},T) implies b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) )
assume that
A2: [a,b] in PolyRedRel ({(0_ (n,L))},T) and
[a,c] in PolyRedRel ({(0_ (n,L))},T) ; :: thesis: b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T)
consider p, q being object such that
A3: p in NonZero (Polynom-Ring (n,L)) and
A4: q in the carrier of (Polynom-Ring (n,L)) and
A5: [a,b] = [p,q] by ;
reconsider q = q as Polynomial of n,L by ;
not p in {(0_ (n,L))} by ;
then p <> 0_ (n,L) by TARSKI:def 1;
then reconsider p = p as non-zero Polynomial of n,L by ;
p reduces_to q,{(0_ (n,L))},T by ;
then consider g being Polynomial of n,L such that
A6: g in {(0_ (n,L))} and
A7: p reduces_to q,g,T by POLYRED:def 7;
g = 0_ (n,L) by ;
then p is_reducible_wrt 0_ (n,L),T by ;
hence b,c are_convergent_wrt PolyRedRel ({(0_ (n,L))},T) by Lm3; :: thesis: verum
end;
then A8: PolyRedRel ({(0_ (n,L))},T) is locally-confluent by REWRITE1:def 24;
0_ (n,L) = 0. (Polynom-Ring (n,L)) by POLYNOM1:def 11;
then {(0_ (n,L))} -Ideal = {(0_ (n,L))} by IDEAL_1:44;
hence {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T by A8; :: thesis: verum