let X be set ; :: thesis: for L being List of X
for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2)
let L be List of X; :: thesis: for O1, O2 being Operation of X holds L \& (O1 AND O2) = (L \& O1) AND (L \& O2)
let O1, O2 be Operation of X; :: thesis: L \& (O1 AND O2) = (L \& O1) AND (L \& O2)
( L \& (O1 AND O2) c= L \& O1 & L \& (O1 AND O2) c= L \& O2 ) by Th26, XBOOLE_1:17;
hence L \& (O1 AND O2) c= (L \& O1) AND (L \& O2) by XBOOLE_1:19; :: according to XBOOLE_0:def 10 :: thesis: (L \& O1) AND (L \& O2) c= L \& (O1 AND O2)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (L \& O1) AND (L \& O2) or z in L \& (O1 AND O2) )
assume z in (L \& O1) AND (L \& O2) ; :: thesis: z in L \& (O1 AND O2)
then A1: ( z in L \& O1 & z in L \& O2 ) by XBOOLE_0:def 4;

now :: thesis: ( { (x . (O1 AND O2)) where x is Element of X : x in L } <> {} & ( for Y being set st Y in { (x . (O1 AND O2)) where x is Element of X : x in L } holds
z in Y ) )

set O = O1 AND O2;
set c = the Element of L;
{ (x . O1) where x is Element of X : x in L } <> {} by A1, SETFAM_1:def 1;
then consider c being object such that
A2: c in { (x . O1) where x is Element of X : x in L } by XBOOLE_0:def 1;
consider a being Element of X such that
A3: ( c = a . O1 & a in L ) by A2;
a . (O1 AND O2) in { (x . (O1 AND O2)) where x is Element of X : x in L } by A3;
hence { (x . (O1 AND O2)) where x is Element of X : x in L } <> {} ; :: thesis: for Y being set st Y in { (x . (O1 AND O2)) where x is Element of X : x in L } holds
z in Y
let Y be set ; :: thesis: ( Y in { (x . (O1 AND O2)) where x is Element of X : x in L } implies z in Y )
assume Y in { (x . (O1 AND O2)) where x is Element of X : x in L } ; :: thesis: z in Y
then consider x being Element of X such that
A4: ( Y = x . (O1 AND O2) & x in L ) ;
A5: Y = (x . O1) AND (x . O2) by A4, RELSET_2:11;
x . O1 in { (y . O1) where y is Element of X : y in L } by A4;
then A6: z in x . O1 by A1, SETFAM_1:def 1;
x . O2 in { (y . O2) where y is Element of X : y in L } by A4;
then z in x . O2 by A1, SETFAM_1:def 1;
hence z in Y by A5, A6, XBOOLE_0:def 4; :: thesis: verum

end;

hence z in L \& (O1 AND O2) by SETFAM_1:def 1; :: thesis: verum