:: deftheorem Def6 defines Zero_ ALGGEO_1:def 5 :
for R being domRing
for n being non empty Ordinal
for S being Subset of (Polynom-Ring (n,R)) holds
( ( S <> {} implies Zero_ S = { x where x is Function of n,R : for p being Polynomial of n,R st p in S holds
eval (p,x) = 0. R } ) & ( not S <> {} implies Zero_ S = {} ) );