theorem :: ALGGEO_1:28

for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds Ideal_ X is Ideal of (Polynom-Ring (n,R))