theorem :: ALGGEO_1:35

for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds Ideal_ (Zero_ (Ideal_ X)) = Ideal_ X by Th32, Th29, Th33;