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 XBOOLE_1:17, Th81;
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 set ; :: 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 A5: ( 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 A5, SETFAM_1:def 1;
then consider c being set such that
A1: 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
A2: ( c = a . O1 & a in L ) by A1;
a . (O1 AND O2) in { (x . (O1 AND O2)) where x is Element of X : x in L } by A2;
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
A3: ( Y = x . (O1 AND O2) & x in L ) ;
A4: Y = (x . O1) AND (x . O2) by A3, RELSET_2:11;
x . O1 in { (y . O1) where y is Element of X : y in L } by A3;
then A6: z in x . O1 by A5, SETFAM_1:def 1;
x . O2 in { (y . O2) where y is Element of X : y in L } by A3;
then z in x . O2 by A5, SETFAM_1:def 1;
hence z in Y by A4, A6, XBOOLE_0:def 4; :: thesis: verum

end;

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