theorem Th33: :: ALGGEO_1:33

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