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;

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

hence
z in L \& (O1 AND O2)
by SETFAM_1:def 1; :: thesis: verumz 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;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