let I be set ; :: thesis: for A, B being ManySortedSet of I st A (\/) B is non-empty & ( for X, Y being ManySortedSet of I st X <> Y & X in A (\/) B & Y in A (\/) B holds
X (/\) Y = EmptyMS I ) holds
union (A (/\) B) = (union A) (/\) (union B)
let A, B be ManySortedSet of I; :: thesis: ( A (\/) B is non-empty & ( for X, Y being ManySortedSet of I st X <> Y & X in A (\/) B & Y in A (\/) B holds
X (/\) Y = EmptyMS I ) implies union (A (/\) B) = (union A) (/\) (union B) )
assume A1: A (\/) B is non-empty ; :: thesis: ( ex X, Y being ManySortedSet of I st
( X <> Y & X in A (\/) B & Y in A (\/) B & not X (/\) Y = EmptyMS I ) or union (A (/\) B) = (union A) (/\) (union B) )
assume A2: for X, Y being ManySortedSet of I st X <> Y & X in A (\/) B & Y in A (\/) B holds
X (/\) Y = EmptyMS I ; :: thesis: union (A (/\) B) = (union A) (/\) (union B)

now :: thesis: for i being object st i in I holds
(union (A (/\) B)) . i = ((union A) (/\) (union B)) . i

let i be object ; :: thesis: ( i in I implies (union (A (/\) B)) . i = ((union A) (/\) (union B)) . i )
assume A3: i in I ; :: thesis: (union (A (/\) B)) . i = ((union A) (/\) (union B)) . i
for X9, Y9 being set st X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) holds
X9 misses Y9

proof

consider M being ManySortedSet of I such that
A4: M in A (\/) B by A1, PBOOLE:134;
A5: i in {i} by TARSKI:def 1;
let X9, Y9 be set ; :: thesis: ( X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) implies X9 misses Y9 )
assume that
A6: X9 <> Y9 and
A7: X9 in (A . i) \/ (B . i) and
A8: Y9 in (A . i) \/ (B . i) ; :: thesis: X9 misses Y9
( dom (M +* (i .--> X9)) = I & dom (M +* (i .--> Y9)) = I ) by A3, Lm1;
then reconsider Kx = M +* (i .--> X9), Ky = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
dom (i .--> Y9) = {i} ;
then A10: Ky . i = (i .--> Y9) . i by A5, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
A11: Ky in A (\/) B

proof

let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or Ky . j in (A (\/) B) . j )
assume A12: j in I ; :: thesis: Ky . j in (A (\/) B) . j

now :: thesis: Ky . j in (A (\/) B) . j

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

suppose j = i ; :: thesis: Ky . j in (A (\/) B) . j

hence Ky . j in (A (\/) B) . j by A8, A10, A12, PBOOLE:def 4; :: thesis: verum

end;

suppose j <> i ; :: thesis: Ky . j in (A (\/) B) . j

then not j in dom (i .--> Y9) by TARSKI:def 1;
then Ky . j = M . j by FUNCT_4:11;
hence Ky . j in (A (\/) B) . j by A4, A12; :: thesis: verum

end;

end;

end;

hence Ky . j in (A (\/) B) . j ; :: thesis: verum

end;

dom (i .--> X9) = {i} ;
then A14: Kx . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
Kx in A (\/) B

proof

let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or Kx . j in (A (\/) B) . j )
assume A15: j in I ; :: thesis: Kx . j in (A (\/) B) . j

now :: thesis: ( ( j = i & Kx . j in (A (\/) B) . j ) or ( j <> i & Kx . j in (A (\/) B) . j ) )

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

case j = i ; :: thesis: Kx . j in (A (\/) B) . j

hence Kx . j in (A (\/) B) . j by A7, A14, A15, PBOOLE:def 4; :: thesis: verum

end;

case j <> i ; :: thesis: Kx . j in (A (\/) B) . j

then not j in dom (i .--> X9) by TARSKI:def 1;
then Kx . j = M . j by FUNCT_4:11;
hence Kx . j in (A (\/) B) . j by A4, A15; :: thesis: verum

end;

end;

end;

hence Kx . j in (A (\/) B) . j ; :: thesis: verum

end;

then Kx (/\) Ky = EmptyMS I by A2, A6, A14, A10, A11;
then (Kx (/\) Ky) . i = {} by PBOOLE:5;
then X9 /\ Y9 = {} by A3, A14, A10, PBOOLE:def 5;
hence X9 misses Y9 by XBOOLE_0:def 7; :: thesis: verum

end;

then union ((A . i) /\ (B . i)) = (union (A . i)) /\ (union (B . i)) by ZFMISC_1:83;
then union ((A . i) /\ (B . i)) = ((union A) . i) /\ (union (B . i)) by A3, Def2;
then union ((A . i) /\ (B . i)) = ((union A) . i) /\ ((union B) . i) by A3, Def2;
then union ((A . i) /\ (B . i)) = ((union A) (/\) (union B)) . i by A3, PBOOLE:def 5;
hence (union (A (/\) B)) . i = ((union A) (/\) (union B)) . i by A3, Lm7; :: thesis: verum

end;

hence union (A (/\) B) = (union A) (/\) (union B) ; :: thesis: verum