:: deftheorem defines Zero_ ALGGEO_1:def 4 :
for R being domRing
for n being non empty Ordinal
for f being Polynomial of n,R holds Zero_ f = { x where x is Function of n,R : eval (f,x) = 0. R } ;