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 non empty Subset of (Polynom-Ring n,L) holds
( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds
f has_a_Standard_Representation_of G,T )
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 non empty Subset of (Polynom-Ring n,L) holds
( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds
f has_a_Standard_Representation_of G,T )
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 non empty Subset of (Polynom-Ring n,L) holds
( G is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in G -Ideal holds
f has_a_Standard_Representation_of G,T )
let P be non empty Subset of (Polynom-Ring n,L); :: thesis: ( P is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in P -Ideal holds
f has_a_Standard_Representation_of P,T )
X: 0_ n,L = 0. (Polynom-Ring n,L) by POLYNOM1:def 27;

A1: now

assume P is_Groebner_basis_wrt T ; :: thesis: for f being non-zero Polynomial of n,L st f in P -Ideal holds
f has_a_Standard_Representation_of P,T
then PolyRedRel P,T is locally-confluent by GROEB_1:def 3;
then PolyRedRel P,T is confluent ;
then PolyRedRel P,T is with_Church-Rosser_property ;
hence for f being non-zero Polynomial of n,L st f in P -Ideal holds
f has_a_Standard_Representation_of P,T by Th43, X, GROEB_1:15; :: thesis: verum

end;

now

assume for f being non-zero Polynomial of n,L st f in P -Ideal holds
f has_a_Standard_Representation_of P,T ; :: thesis: P is_Groebner_basis_wrt T
then for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T by Th44;
then for b being bag of st b in HT (P -Ideal ),T holds
ex b' being bag of st
( b' in HT P,T & b' divides b ) by GROEB_1:18;
then HT (P -Ideal ),T c= multiples (HT P,T) by GROEB_1:19;
then PolyRedRel P,T is locally-confluent by GROEB_1:20;
hence P is_Groebner_basis_wrt T by GROEB_1:def 3; :: thesis: verum

end;

hence ( P is_Groebner_basis_wrt T iff for f being non-zero Polynomial of n,L st f in P -Ideal holds
f has_a_Standard_Representation_of P,T ) by A1; :: thesis: verum