let R be domRing; :: thesis: for n being non empty Ordinal
for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I *' J) = (Zero_ I) \/ (Zero_ J)
let n be non empty Ordinal; :: thesis: for I, J being Ideal of (Polynom-Ring (n,R)) holds Zero_ (I *' J) = (Zero_ I) \/ (Zero_ J)
let I, J be Ideal of (Polynom-Ring (n,R)); :: thesis: Zero_ (I *' J) = (Zero_ I) \/ (Zero_ J)
set PR = Polynom-Ring (n,R);
A1: Zero_ (I /\ J) c= Zero_ (I *' J) by Th16, IDEAL_1:79;
for o being object st o in Zero_ (I *' J) holds
o in (Zero_ I) \/ (Zero_ J)

proof

let o be object ; :: thesis: ( o in Zero_ (I *' J) implies o in (Zero_ I) \/ (Zero_ J) )
assume o in Zero_ (I *' J) ; :: thesis: o in (Zero_ I) \/ (Zero_ J)
then o in { x where x is Function of n,R : for p being Polynomial of n,R st p in I *' J holds
eval (p,x) = 0. R } by Def6;
then consider x1 being Function of n,R such that
A3: ( o = x1 & ( for p being Polynomial of n,R st p in I *' J holds
eval (p,x1) = 0. R ) ) ;
x1 in (Zero_ I) \/ (Zero_ J)

proof

assume not x1 in (Zero_ I) \/ (Zero_ J) ; :: thesis: contradiction
then A5: ( not x1 in Zero_ I & not x1 in Zero_ J ) by XBOOLE_0:def 3;
then not x1 in { z where z is Function of n,R : for f being Polynomial of n,R st f in I holds
eval (f,z) = 0. R } by Def6;
then consider f1 being Polynomial of n,R such that
A6: ( f1 in I & eval (f1,x1) <> 0. R ) ;
not x1 in { z where z is Function of n,R : for f being Polynomial of n,R st f in J holds
eval (f,z) = 0. R } by A5, Def6;
then consider f2 being Polynomial of n,R such that
A7: ( f2 in J & eval (f2,x1) <> 0. R ) ;
reconsider F1 = f1, F2 = f2 as Element of (Polynom-Ring (n,R)) by POLYNOM1:def 11;
A8: F1 * F2 = f1 *' f2 by POLYNOM1:def 11;
reconsider s1 = <*(F1 * F2)*> as FinSequence of the carrier of (Polynom-Ring (n,R)) ;
dom s1 = Seg 1 by FINSEQ_1:def 8;
then A10: len s1 = 1 by FINSEQ_1:def 3;
A11: Sum s1 = F1 * F2 by BINOM:3;
set M = { (Sum s) where s is FinSequence of the carrier of (Polynom-Ring (n,R)) : for i being Element of NAT st 1 <= i & i <= len s holds
ex a, b being Element of (Polynom-Ring (n,R)) st
( s . i = a * b & a in I & b in J ) } ;
for i being Element of NAT st 1 <= i & i <= len s1 holds
ex a, b being Element of (Polynom-Ring (n,R)) st
( s1 . i = a * b & a in I & b in J )

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len s1 implies ex a, b being Element of (Polynom-Ring (n,R)) st
( s1 . i = a * b & a in I & b in J ) )
assume ( 1 <= i & i <= len s1 ) ; :: thesis: ex a, b being Element of (Polynom-Ring (n,R)) st
( s1 . i = a * b & a in I & b in J )
then A13: i = 1 by A10, XXREAL_0:1;
consider a, b being Element of (Polynom-Ring (n,R)) such that
A14: ( a = F1 & b = F2 & s1 . i = a * b & a in I & b in J ) by A6, A7, A13;
thus ex a, b being Element of (Polynom-Ring (n,R)) st
( s1 . i = a * b & a in I & b in J ) by A14; :: thesis: verum

end;

then f1 *' f2 in I *' J by A8, A11;
then 0. R = eval ((f1 *' f2),x1) by A3
.= (eval (f1,x1)) * (eval (f2,x1)) by POLYNOM2:25 ;
hence contradiction by A6, A7, VECTSP_2:def 1; :: thesis: verum

end;

hence o in (Zero_ I) \/ (Zero_ J) by A3; :: thesis: verum

end;

then Zero_ (I *' J) c= (Zero_ I) \/ (Zero_ J) ;
hence Zero_ (I *' J) = (Zero_ I) \/ (Zero_ J) by A1, Th22; :: thesis: verum