defpred S1[ object , object ] means ( Im (O,$1) = {} & $2 = $1 );
consider O1 being Relation such that
A1: for a, b being object holds
( [a,b] in O1 iff ( a in X & b in X & S1[a,b] ) ) from RELAT_1:sch 1();
 O1 c= [:X,X:]
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in O1 or [x,y] in [:X,X:] )
assume [x,y] in O1 ; :: thesis: [x,y] in [:X,X:]
then ( x in X & y in X ) by A1;
hence [x,y] in [:X,X:] by ZFMISC_1:87; :: thesis: verum
end;
then reconsider O1 = O1 as Operation of X ;
take O1 ; :: thesis: for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
let L be List of X; :: thesis: L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
thus L | O1 c= union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } c= L | O1
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in L | O1 or a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } )
assume a in L | O1 ; :: thesis: a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
then consider b being Element of X such that
A2: ( a in b . O1 & b in L ) by Th23;
[b,a] in O1 by A2, RELAT_1:169;
then A3: ( a = b & b . O = {} ) by A1;
then B1: a in {b} by TARSKI:def 1;
reconsider Z = IFEQ ((b . O),{},{b},{}) as set ;
A4: a in Z by A3, B1, FUNCOP_1:def 8;
IFEQ ((b . O),{},{b},{}) in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by A2;
hence a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by A4, TARSKI:def 4; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } or a in L | O1 )
assume a in union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ; :: thesis: a in L | O1
then consider A being set such that
A5: ( a in A & A in { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) by TARSKI:def 4;
consider x being Element of X such that
A6: ( A = IFEQ ((x . O),{},{x},{}) & x in L ) by A5;
A7: x . O = {} by A5, A6, FUNCOP_1:def 8;
then A = {x} by A6, FUNCOP_1:def 8;
then a = x by A5, TARSKI:def 1;
then [x,a] in O1 by A1, A6, A7;
hence a in L | O1 by A6, RELAT_1:def 13; :: thesis: verum