A8:
for O being Operation of X st O = O2 OR holds

for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

thus ( O = O2 OR implies for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by A8; :: thesis: ( ( for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) implies O = O2 OR )

assume A14: for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ; :: thesis: O = O2 OR

for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

proof

let O be Operation of X; :: thesis: ( O = O2 OR iff for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } )
let O be Operation of X; :: thesis: ( O = O2 OR implies for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } )

assume A9: O = O1 \/ O2 ; :: thesis: for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

defpred S_{1}[ set , set ] means ( [$1,$2] in O1 or [$1,$2] in O2 );

let L be List of X; :: thesis: L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

thus L | O c= union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } c= L | O

assume z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ; :: thesis: z in L | O

then consider Y being set such that

A11: ( z in Y & Y in { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by TARSKI:def 4;

consider x being Element of X such that

A12: ( Y = (x . O1) OR (x . O2) & x in L ) by A11;

A13: ( z in x . O1 or z in x . O2 ) by A11, A12, XBOOLE_0:def 3;

reconsider z = z as Element of X by A11, A12;

( [x,z] in O1 or [x,z] in O2 ) by A13, RELAT_1:169;

then [x,z] in O by A9, XBOOLE_0:def 3;

hence z in L | O by A12, RELAT_1:def 13; :: thesis: verum

end;assume A9: O = O1 \/ O2 ; :: thesis: for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

defpred S

let L be List of X; :: thesis: L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

thus L | O c= union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } :: according to XBOOLE_0:def 10 :: thesis: union { ((x . O1) OR (x . 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 union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } or z in L | O )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L | O or z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } )

assume z in L | O ; :: thesis: z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

then consider y being object such that

A10: ( [y,z] in O & y in L ) by RELAT_1:def 13;

reconsider y = y, z = z as Element of X by A10, ZFMISC_1:87;

( [y,z] in O1 or [y,z] in O2 ) by A9, A10, XBOOLE_0:def 3;

then ( z in y . O1 or z in y . O2 ) by RELAT_1:169;

then ( z in (y . O1) OR (y . O2) & (y . O1) OR (y . O2) in { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by A10, XBOOLE_0:def 3;

hence z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } by TARSKI:def 4; :: thesis: verum

end;assume z in L | O ; :: thesis: z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L }

then consider y being object such that

A10: ( [y,z] in O & y in L ) by RELAT_1:def 13;

reconsider y = y, z = z as Element of X by A10, ZFMISC_1:87;

( [y,z] in O1 or [y,z] in O2 ) by A9, A10, XBOOLE_0:def 3;

then ( z in y . O1 or z in y . O2 ) by RELAT_1:169;

then ( z in (y . O1) OR (y . O2) & (y . O1) OR (y . O2) in { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by A10, XBOOLE_0:def 3;

hence z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } by TARSKI:def 4; :: thesis: verum

assume z in union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ; :: thesis: z in L | O

then consider Y being set such that

A11: ( z in Y & Y in { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by TARSKI:def 4;

consider x being Element of X such that

A12: ( Y = (x . O1) OR (x . O2) & x in L ) by A11;

A13: ( z in x . O1 or z in x . O2 ) by A11, A12, XBOOLE_0:def 3;

reconsider z = z as Element of X by A11, A12;

( [x,z] in O1 or [x,z] in O2 ) by A13, RELAT_1:169;

then [x,z] in O by A9, XBOOLE_0:def 3;

hence z in L | O by A12, RELAT_1:def 13; :: thesis: verum

thus ( O = O2 OR implies for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) by A8; :: thesis: ( ( for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ) implies O = O2 OR )

assume A14: for L being List of X holds L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } ; :: thesis: O = O2 OR

now :: thesis: for L being List of X holds L | O = L | (O1 \/ O2)

hence
O = O2 OR
by Th30; :: thesis: verumlet L be List of X; :: thesis: L | O = L | (O1 \/ O2)

thus L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } by A14

.= L | (O1 \/ O2) by A8 ; :: thesis: verum

end;thus L | O = union { ((x . O1) OR (x . O2)) where x is Element of X : x in L } by A14

.= L | (O1 \/ O2) by A8 ; :: thesis: verum