theorem :: POLYNOM7:17

for X being set
for L being non empty ZeroStr
for p being Series of X,L holds
( p is ConstPoly of X,L iff ex a being Element of L st p = a | (X,L) )