theorem :: POLYNOM7:2

for X being set
for R being non empty ZeroStr holds
( not R is trivial iff ex s being Series of X,R st Support s <> {} )