:: deftheorem defines polyset ALGGEO_1:def 8 :
for n being non empty Ordinal
for R being domRing
for a being Function of n,R holds polyset a = { f where f is Polynomial of n,R : ex i being Element of n st f = deg1Poly (a,i) } ;