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 = [0] 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 = [0] 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 = [0] 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 = [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

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

end;

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

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

end;

end;

end;

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

end;

A13: dom (i .--> X') = {i} by FUNCOP_1:19;
then A14: Kx . i = (i .--> X') . i by A5, FUNCT_4:14
.= X' by FUNCOP_1:87 ;
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 A7, A14, 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 A13, TARSKI:def 1;
then Kx . j = M . j by FUNCT_4:12;
hence Kx . j in (A \/ B) . j by A4, A15, PBOOLE:def 4; :: thesis: verum

end;

end;

end;

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

end;

then Kx /\ Ky = [0] I by A2, A6, A14, A10, A11;
then (Kx /\ Ky) . i = {} by PBOOLE:5;
then X' /\ Y' = {} by A3, A14, A10, 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