:: deftheorem defines has_a_Standard_Representation_of GROEB_2:def 10 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for f being Polynomial of n,L
for P being non empty Subset of (Polynom-Ring (n,L)) holds
( f has_a_Standard_Representation_of P,T iff ex A being LeftLinearCombination of P st A is_Standard_Representation_of f,P,T );