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)
A1: Zero_ (I \/ J) c= (Zero_ I) /\ (Zero_ J)

proof

( Zero_ (I \/ J) c= Zero_ J & Zero_ (I \/ J) c= Zero_ I ) by XBOOLE_1:7, Th16;
hence Zero_ (I \/ J) c= (Zero_ I) /\ (Zero_ J) by XBOOLE_1:19; :: thesis: verum

end;

(Zero_ I) /\ (Zero_ J) c= Zero_ (I \/ J)

proof

for o being object st o in (Zero_ I) /\ (Zero_ J) holds
o in Zero_ (I \/ J)

proof

let o be object ; :: thesis: ( o in (Zero_ I) /\ (Zero_ J) implies o in Zero_ (I \/ J) )
assume o in (Zero_ I) /\ (Zero_ J) ; :: thesis: o in Zero_ (I \/ J)
then A3: ( o in Zero_ I & o in Zero_ J ) by XBOOLE_0:def 4;
then o in { x where x is Function of n,R : for f being Polynomial of n,R st f in J holds
eval (f,x) = 0. R } by Def6;
then consider x being Function of n,R such that
A4: ( o = x & ( for f being Polynomial of n,R st f in J holds
eval (f,x) = 0. R ) ) ;
o in { x where x is Function of n,R : for f being Polynomial of n,R st f in I holds
eval (f,x) = 0. R } by A3, Def6;
then consider y being Function of n,R such that
A5: ( o = y & ( for g being Polynomial of n,R st g in I holds
eval (g,y) = 0. R ) ) ;
o in Zero_ (I \/ J)

proof

assume not o in Zero_ (I \/ J) ; :: thesis: contradiction
then A7: not o in { x where x is Function of n,R : for f being Polynomial of n,R st f in I \/ J holds
eval (f,x) = 0. R } by Def6;
consider f being Polynomial of n,R such that
A8: ( f in I \/ J & eval (f,x) <> 0. R ) by A4, A7;

per cases ( f in J or f in I ) by A8, XBOOLE_0:def 3;

suppose f in J ; :: thesis: contradiction

hence contradiction by A8, A4; :: thesis: verum

end;

suppose f in I ; :: thesis: contradiction

hence contradiction by A8, A4, A5; :: thesis: verum

end;

end;

end;

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

end;

hence (Zero_ I) /\ (Zero_ J) c= Zero_ (I \/ J) ; :: thesis: verum

end;

hence Zero_ (I \/ J) = (Zero_ I) /\ (Zero_ J) by A1; :: thesis: verum