theorem :: ALGGEO_1:31

for R being domRing
for n being non empty Ordinal holds {(0. (Polynom-Ring (n,R)))} c= Ideal_ ([#] (Funcs (n,([#] R))))