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

now

let i be set ; :: 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 X', Y' being set st X' <> Y' & X' in (A . i) \/ (B . i) & Y' in (A . i) \/ (B . i) holds
X' misses Y'

proof

let X', Y' be set ; :: thesis: ( X' <> Y' & X' in (A . i) \/ (B . i) & Y' in (A . i) \/ (B . i) implies X' misses Y' )
assume that
A4: X' <> Y' and
A5: X' in (A . i) \/ (B . i) and
A6: Y' in (A . i) \/ (B . i) ; :: thesis: X' misses Y'
consider M being ManySortedSet of such that
A7: M in A \/ B by A1, PBOOLE:146;
A8: dom (i .--> X') = {i} by FUNCOP_1:19;
A9: dom (M +* (i .--> X')) = I by A3, Lm1;
A10: dom (i .--> Y') = {i} by FUNCOP_1:19;
dom (M +* (i .--> Y')) = I by A3, Lm1;
then reconsider Kx = M +* (i .--> X'), Ky = M +* (i .--> Y') as ManySortedSet of by A9, PARTFUN1:def 4, RELAT_1:def 18;
A11: i in {i} by TARSKI:def 1;
then A12: Kx . i = (i .--> X') . i by A8, FUNCT_4:14
.= X' by FUNCOP_1:87 ;
A13: Ky . i = (i .--> Y') . i by A10, A11, FUNCT_4:14
.= Y' by FUNCOP_1:87 ;
A14: Kx in A \/ B

proof

let j be set ; :: according to PBOOLE:def 4 :: 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

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 A5, A12, A15, PBOOLE:def 7; :: thesis: verum

end;

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

then not j in dom (i .--> X') by A8, TARSKI:def 1;
then Kx . j = M . j by FUNCT_4:12;
hence Kx . j in (A \/ B) . j by A7, A15, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

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

end;

Ky in A \/ B

proof

let j be set ; :: according to PBOOLE:def 4 :: thesis: ( not j in I or Ky . j in (A \/ B) . j )
assume A16: j in I ; :: thesis: Ky . j in (A \/ B) . j

now

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 A6, A13, A16, PBOOLE:def 7; :: thesis: verum

end;

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

then not j in dom (i .--> Y') by A10, TARSKI:def 1;
then Ky . j = M . j by FUNCT_4:12;
hence Ky . j in (A \/ B) . j by A7, A16, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

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

end;

then Kx /\ Ky = [0] I by A2, A4, A12, A13, A14;
then (Kx /\ Ky) . i = {} by PBOOLE:5;
then X' /\ Y' = {} by A3, A12, A13, PBOOLE:def 8;
hence X' misses Y' by XBOOLE_0:def 7; :: thesis: verum

end;

then union ((A . i) /\ (B . i)) = (union (A . i)) /\ (union (B . i)) by ZFMISC_1:101;
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 8;
hence (union (A /\ B)) . i = ((union A) /\ (union B)) . i by A3, Lm7; :: thesis: verum

end;

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