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

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;

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 \& O) AND (L2 \& O) or z in (L1 OR L2) \& O )
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)

hence z in (L1 \& O) AND (L2 \& O) by A4, XBOOLE_0:def 4; :: thesis: verum

end;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 ) )

then A4:
z in L1 \& O
by SETFAM_1:def 1;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;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

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 ) )

then
z in L2 \& O
by SETFAM_1:def 1;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;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

hence z in (L1 \& O) AND (L2 \& O) by A4, XBOOLE_0:def 4; :: thesis: verum

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 ) )

hence
z in (L1 OR L2) \& O
by SETFAM_1:def 1; :: thesis: verumz 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;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