:: deftheorem Def5 defines finite-Support POLYNOM1:def 5 :
for S being ZeroStr
for p being the carrier of b₁ -valued Function holds
( p is finite-Support iff Support p is finite );