defpred S₁[ set , set ] means ex x being Element of X st
( $1 = x & $2 in (x . O1) \& O2 );
consider O being Relation such that
A1: for z, s being set holds
( [z,s] in O iff ( z in X & s in X & S₁[z,s] ) ) from RELAT_1:sch 1();
O c= [:X,X:]

proof

let z be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [z,b₁] in O or [z,b₁] in [:X,X:] )
let s be set ; :: 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 A1;
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 set ; :: 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
A2: ( z in y . O & y in L ) by Th1;
[y,z] in O by A2, RELAT_1:169;
then ex x being Element of X st
( y = x & z in (x . O1) \& O2 ) by A1;
then ( z in (y . O1) \& O2 & (y . O1) \& O2 in { ((x . O1) \& O2) where x is Element of X : x in L } ) by A2;
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 set ; :: 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
A3: ( 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
A4: ( Y = (x . O1) \& O2 & x in L ) by A3;
[x,z] in O by A1, A3, A4;
hence z in L | O by A4, RELAT_1:def 13; :: thesis: verum