theorem Th30: :: ALGGEO_1:30

for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds
( X = {} iff Ideal_ X = [#] (Polynom-Ring (n,R)) )