defpred S1[ object , object ] means ex x being Element of X st
( $1 = x & $2 in (x . O1) \& O2 );
consider O being Relation such that
A23: for z, s being object holds
( [z,s] in O iff ( z in X & s in X & S1[z,s] ) ) from RELAT_1:sch 1();
 O c= [:X,X:]
proof
let z, s be object ; :: according to RELAT_1:def 3 :: thesis: ( not [z,s] in O or [z,s] in [:X,X:] )
assume [z,s] in O ; :: thesis: [z,s] in [:X,X:]
then ( z in X & s in X ) by A23;
hence [z,s] in [:X,X:] by ZFMISC_1:87; :: thesis: verum
end;
then reconsider O = O as Operation of X ;
take O ; :: thesis: for L being List of X holds L | O = union { ((x . O1) \& O2) where x is Element of X : x in L }
let L be List of X; :: thesis: L | O = union { ((x . O1) \& O2) where x is Element of X : x in L }
thus L | O c= union { ((x . O1) \& O2) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { ((x . O1) \& O2) where x is Element of X : x in L } c= L | O
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L | O or z in union { ((x . O1) \& O2) where x is Element of X : x in L } )
assume z in L | O ; :: thesis: z in union { ((x . O1) \& O2) where x is Element of X : x in L }
then consider y being Element of X such that
A24: ( z in y . O & y in L ) by Th23;
[y,z] in O by A24, RELAT_1:169;
then ex x being Element of X st
( y = x & z in (x . O1) \& O2 ) by A23;
then ( z in (y . O1) \& O2 & (y . O1) \& O2 in { ((x . O1) \& O2) where x is Element of X : x in L } ) by A24;
hence z in union { ((x . O1) \& O2) where x is Element of X : x in L } by TARSKI:def 4; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union { ((x . O1) \& O2) where x is Element of X : x in L } or z in L | O )
assume z in union { ((x . O1) \& O2) where x is Element of X : x in L } ; :: thesis: z in L | O
then consider Y being set such that
A25: ( z in Y & Y in { ((x . O1) \& O2) where x is Element of X : x in L } ) by TARSKI:def 4;
consider x being Element of X such that
A26: ( Y = (x . O1) \& O2 & x in L ) by A25;
[x,z] in O by A23, A25, A26;
hence z in L | O by A26, RELAT_1:def 13; :: thesis: verum