defpred S_{1}[ 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 & S_{1}[a,b] ) )
from RELAT_1:sch 1();

O1 c= [:X,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

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

consider O1 being Relation such that

A1: for a, b being object holds

( [a,b] in O1 iff ( a in X & b in X & S

O1 c= [:X,X:]

proof

then reconsider O1 = O1 as Operation of X ;
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;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

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 union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } or a in L | O1 )
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;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

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