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) = () \ ()

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) = () \ () )

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) = () \ ()
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 ;
set W = Y . i;
V1: (Y (\) Z) . i = (Y . i) \ (Z . i) by ;
S82: Y . i in rng Y by ;
S9: x in union (rng Y) by ;
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 ;
end;
hence x in (union (rng Y)) \ (union (rng Z)) by ; :: 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 ;
consider i being object such that
S7: ( i in dom Y & K = Y . i ) by ;
not x in Z . i
proof
assume S81: x in Z . i ; :: thesis: contradiction
Z . i in rng Z by ;
hence contradiction by A3, S81, TARSKI:def 4; :: thesis: verum
end;
then S9: x in (Y . i) \ (Z . i) by ;
S10: x in (Y (\) Z) . i by ;
(Y (\) Z) . i in rng (Y (\) Z) by ;
hence x in union (rng (Y (\) Z)) by ; :: 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) = () \ () by ; :: thesis: verum