theorem :: ALGGEO_1:39

for R being domRing
for n being non empty Ordinal
for X being Subset of (Funcs (n,([#] R))) holds sqrt (Ideal_ X) = Ideal_ X