theorem :: ALGGEO_1:23

for R being domRing
for n being non empty Ordinal
for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I *' J) = (Zero_ I) \/ (Zero_ J)