let X be set ; :: thesis: for L1, L2 being List of X
for O being Operation of X st L1 <> {} & L2 <> {} holds
(L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)
let L1, L2 be List of X; :: thesis: for O being Operation of X st L1 <> {} & L2 <> {} holds
(L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)
let O be Operation of X; :: thesis: ( L1 <> {} & L2 <> {} implies (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O) )
assume A1: ( L1 <> {} & L2 <> {} ) ; :: thesis: (L1 OR L2) \& O = (L1 \& O) AND (L2 \& O)
thus (L1 OR L2) \& O c= (L1 \& O) AND (L2 \& O) :: according to XBOOLE_0:def 10 :: thesis: (L1 \& O) AND (L2 \& O) c= (L1 OR L2) \& O
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (L1 OR L2) \& O or z in (L1 \& O) AND (L2 \& O) )
assume A2: z in (L1 OR L2) \& O ; :: thesis: z in (L1 \& O) AND (L2 \& O)
now :: thesis: ( { (x . O) where x is Element of X : x in L1 } <> {} & ( for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds
z in Y ) )
set c = the Element of L1;
the Element of L1 in L1 by A1;
then reconsider c = the Element of L1 as Element of X ;
c . O in { (x . O) where x is Element of X : x in L1 } by A1;
hence { (x . O) where x is Element of X : x in L1 } <> {} ; :: thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 } holds
z in Y
let Y be set ; :: thesis: ( Y in { (x . O) where x is Element of X : x in L1 } implies z in Y )
assume Y in { (x . O) where x is Element of X : x in L1 } ; :: thesis: z in Y
then consider x being Element of X such that
A3: ( Y = x . O & x in L1 ) ;
x in L1 OR L2 by A3, XBOOLE_0:def 3;
then Y in { (a . O) where a is Element of X : a in L1 OR L2 } by A3;
hence z in Y by A2, SETFAM_1:def 1; :: thesis: verum
end;
then A4: z in L1 \& O by SETFAM_1:def 1;
now :: thesis: ( { (x . O) where x is Element of X : x in L2 } <> {} & ( for Y being set st Y in { (x . O) where x is Element of X : x in L2 } holds
z in Y ) )
set c = the Element of L2;
the Element of L2 in L2 by A1;
then reconsider c = the Element of L2 as Element of X ;
c . O in { (x . O) where x is Element of X : x in L2 } by A1;
hence { (x . O) where x is Element of X : x in L2 } <> {} ; :: thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L2 } holds
z in Y
let Y be set ; :: thesis: ( Y in { (x . O) where x is Element of X : x in L2 } implies z in Y )
assume Y in { (x . O) where x is Element of X : x in L2 } ; :: thesis: z in Y
then consider x being Element of X such that
A5: ( Y = x . O & x in L2 ) ;
x in L1 OR L2 by A5, XBOOLE_0:def 3;
then Y in { (a . O) where a is Element of X : a in L1 OR L2 } by A5;
hence z in Y by A2, SETFAM_1:def 1; :: thesis: verum
end;
then z in L2 \& O by SETFAM_1:def 1;
hence z in (L1 \& O) AND (L2 \& O) by A4, XBOOLE_0:def 4; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (L1 \& O) AND (L2 \& O) or z in (L1 OR L2) \& O )
assume z in (L1 \& O) AND (L2 \& O) ; :: thesis: z in (L1 OR L2) \& O
then A6: ( z in L1 \& O & z in L2 \& O ) by XBOOLE_0:def 4;
now :: thesis: ( { (x . O) where x is Element of X : x in L1 OR L2 } <> {} & ( for Y being set st Y in { (x . O) where x is Element of X : x in L1 OR L2 } holds
z in Y ) )
set c = the Element of L2;
the Element of L2 in L2 by A1;
then reconsider c = the Element of L2 as Element of X ;
c in L1 OR L2 by A1, XBOOLE_0:def 3;
then c . O in { (x . O) where x is Element of X : x in L1 OR L2 } ;
hence { (x . O) where x is Element of X : x in L1 OR L2 } <> {} ; :: thesis: for Y being set st Y in { (x . O) where x is Element of X : x in L1 OR L2 } holds
z in Y
let Y be set ; :: thesis: ( Y in { (x . O) where x is Element of X : x in L1 OR L2 } implies z in Y )
assume Y in { (x . O) where x is Element of X : x in L1 OR L2 } ; :: thesis: z in Y
then consider x being Element of X such that
A7: ( Y = x . O & x in L1 OR L2 ) ;
( x in L1 or x in L2 ) by A7, XBOOLE_0:def 3;
then ( Y in { (a . O) where a is Element of X : a in L1 } or Y in { (b . O) where b is Element of X : b in L2 } ) by A7;
hence z in Y by A6, SETFAM_1:def 1; :: thesis: verum
end;
hence z in (L1 OR L2) \& O by SETFAM_1:def 1; :: thesis: verum