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)) )

proof

let x be object ; :: thesis: ( x in union (rng (Y (\) Z)) iff x in (union (rng Y)) \ (union (rng Z)) )

hereby :: thesis: ( x in (union (rng Y)) \ (union (rng Z)) implies 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)

proof

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;

per cases ( i = j or i <> j ) ;

suppose i = j ; :: thesis: contradiction

hence contradiction by V1, S61, S71, XBOOLE_0:def 5, S101, S113; :: thesis: verum

end;

suppose i <> j ; :: thesis: contradiction

then (Y . i) /\ (Z . j) = {} by A2, S7, S112;
hence contradiction by XBOOLE_0:def 4, S113, S101, S71, S61, V1; :: thesis: verum

end;

end;

end;

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

end;

assume A03: x in (union (rng Y)) \ (union (rng Z)) ; :: thesis: x in union (rng (Y (\) 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

proof

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;

then S9: x in (Y . i) \ (Z . i) by S6, S7, XBOOLE_0:def 5;
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;

( Union (Y (\) Z) = union (rng (Y (\) Z)) & Union Y = union (rng Y) & Union Z = union (rng Z) ) by CARD_3:def 4;
hence Union (Y (\) Z) = (Union Y) \ (Union Z) by x, TARSKI:2; :: thesis: verum