for R being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Nat
for b being bag of n
for p1 being Polynomial of n,R
for F being FinSequence of the carrier of (Polynom-Ring (n,R)) st p1 = Sum F holds
ex g being Function of the carrier of (Polynom-Ring (n,R)), the carrier of R st
( ( for p being Polynomial of n,R holds g . p = p . b ) & p1 . b = Sum (g * F) )