:: deftheorem defines is_MonomialRepresentation_of GROEB_2:def 6 :
for n being Ordinal
for L being 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))
for A being LeftLinearCombination of P holds
( A is_MonomialRepresentation_of f iff ( Sum A = f & ( for i being Element of NAT st i in dom A holds
ex m being Monomial of n,L ex p being Polynomial of n,L st
( p in P & A /. i = m *' p ) ) ) );