let I be set ; :: thesis: for Y, Z being ManySortedSet of I st ( for i, j being object st i in I & j in I & i <> j holds

(Y . i) /\ (Z . j) = {} ) holds

Union (Y (\) Z) = (Union Y) \ (Union Z)

let Y, Z be ManySortedSet of I; :: thesis: ( ( for i, j being object st i in I & j in I & i <> j holds

(Y . i) /\ (Z . j) = {} ) implies Union (Y (\) Z) = (Union Y) \ (Union Z) )

set X = Y (\) Z;

assume A2: for i, j being object st i in I & j in I & i <> j holds

(Y . i) /\ (Z . j) = {} ; :: thesis: Union (Y (\) Z) = (Union Y) \ (Union Z)

P0: dom (Y (\) Z) = I by PARTFUN1:def 2;

R0: dom Y = I by PARTFUN1:def 2;

Q0: dom Z = I by PARTFUN1:def 2;

x: for x being object holds

( x in union (rng (Y (\) Z)) iff x in (union (rng Y)) \ (union (rng Z)) )

hence Union (Y (\) Z) = (Union Y) \ (Union Z) by x, TARSKI:2; :: thesis: verum

(Y . i) /\ (Z . j) = {} ) holds

Union (Y (\) Z) = (Union Y) \ (Union Z)

let Y, Z be ManySortedSet of I; :: thesis: ( ( for i, j being object st i in I & j in I & i <> j holds

(Y . i) /\ (Z . j) = {} ) implies Union (Y (\) Z) = (Union Y) \ (Union Z) )

set X = Y (\) Z;

assume A2: for i, j being object st i in I & j in I & i <> j holds

(Y . i) /\ (Z . j) = {} ; :: thesis: Union (Y (\) Z) = (Union Y) \ (Union Z)

P0: dom (Y (\) Z) = I by PARTFUN1:def 2;

R0: dom Y = I by PARTFUN1:def 2;

Q0: dom Z = I by PARTFUN1:def 2;

x: for x being object holds

( x in union (rng (Y (\) Z)) iff x in (union (rng Y)) \ (union (rng Z)) )

proof

( Union (Y (\) Z) = union (rng (Y (\) Z)) & Union Y = union (rng Y) & Union Z = union (rng Z) )
by CARD_3:def 4;
let x be object ; :: thesis: ( x in union (rng (Y (\) Z)) iff x in (union (rng Y)) \ (union (rng Z)) )

then A3: ( x in union (rng Y) & not x in union (rng Z) ) by XBOOLE_0:def 5;

consider K being set such that

S6: ( x in K & K in rng Y ) by TARSKI:def 4, A03;

consider i being object such that

S7: ( i in dom Y & K = Y . i ) by S6, FUNCT_1:def 3;

not x in Z . i

S10: x in (Y (\) Z) . i by S7, S9, PBOOLE:def 6;

(Y (\) Z) . i in rng (Y (\) Z) by S7, P0, FUNCT_1:3;

hence x in union (rng (Y (\) Z)) by S10, TARSKI:def 4; :: thesis: verum

end;hereby :: thesis: ( x in (union (rng Y)) \ (union (rng Z)) implies x in union (rng (Y (\) Z)) )

assume A03:
x in (union (rng Y)) \ (union (rng Z))
; :: thesis: x in union (rng (Y (\) Z))assume
x in union (rng (Y (\) Z))
; :: thesis: x in (union (rng Y)) \ (union (rng Z))

then consider K being set such that

S61: x in K and

S62: K in rng (Y (\) Z) by TARSKI:def 4;

consider i being object such that

S7: i in dom (Y (\) Z) and

S71: K = (Y (\) Z) . i by FUNCT_1:def 3, S62;

set W = Y . i;

V1: (Y (\) Z) . i = (Y . i) \ (Z . i) by PBOOLE:def 6, S7;

S82: Y . i in rng Y by FUNCT_1:3, R0, S7;

S9: x in union (rng Y) by TARSKI:def 4, S71, S61, V1, S82;

not x in union (rng Z)

end;then consider K being set such that

S61: x in K and

S62: K in rng (Y (\) Z) by TARSKI:def 4;

consider i being object such that

S7: i in dom (Y (\) Z) and

S71: K = (Y (\) Z) . i by FUNCT_1:def 3, S62;

set W = Y . i;

V1: (Y (\) Z) . i = (Y . i) \ (Z . i) by PBOOLE:def 6, S7;

S82: Y . i in rng Y by FUNCT_1:3, R0, S7;

S9: x in union (rng Y) by TARSKI:def 4, S71, S61, V1, S82;

not x in union (rng Z)

proof

hence
x in (union (rng Y)) \ (union (rng Z))
by S9, XBOOLE_0:def 5; :: thesis: verum
assume
x in union (rng Z)
; :: thesis: contradiction

then consider L being set such that

S101: x in L and

S102: L in rng Z by TARSKI:def 4;

consider j being object such that

S112: j in dom Z and

S113: L = Z . j by S102, FUNCT_1:def 3;

end;then consider L being set such that

S101: x in L and

S102: L in rng Z by TARSKI:def 4;

consider j being object such that

S112: j in dom Z and

S113: L = Z . j by S102, FUNCT_1:def 3;

then A3: ( x in union (rng Y) & not x in union (rng Z) ) by XBOOLE_0:def 5;

consider K being set such that

S6: ( x in K & K in rng Y ) by TARSKI:def 4, A03;

consider i being object such that

S7: ( i in dom Y & K = Y . i ) by S6, FUNCT_1:def 3;

not x in Z . i

proof

then S9:
x in (Y . i) \ (Z . i)
by S6, S7, XBOOLE_0:def 5;
assume S81:
x in Z . i
; :: thesis: contradiction

Z . i in rng Z by S7, Q0, FUNCT_1:3;

hence contradiction by A3, S81, TARSKI:def 4; :: thesis: verum

end;Z . i in rng Z by S7, Q0, FUNCT_1:3;

hence contradiction by A3, S81, TARSKI:def 4; :: thesis: verum

S10: x in (Y (\) Z) . i by S7, S9, PBOOLE:def 6;

(Y (\) Z) . i in rng (Y (\) Z) by S7, P0, FUNCT_1:3;

hence x in union (rng (Y (\) Z)) by S10, TARSKI:def 4; :: thesis: verum

hence Union (Y (\) Z) = (Union Y) \ (Union Z) by x, TARSKI:2; :: thesis: verum