let I be set ; :: thesis: for B being ManySortedSet of I
for A being non-empty ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X (/\) B = EmptyMS I ) holds
(union A) (/\) B = EmptyMS I
let B be ManySortedSet of I; :: thesis: for A being non-empty ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X (/\) B = EmptyMS I ) holds
(union A) (/\) B = EmptyMS I
let A be non-empty ManySortedSet of I; :: thesis: ( ( for X being ManySortedSet of I st X in A holds
X (/\) B = EmptyMS I ) implies (union A) (/\) B = EmptyMS I )
assume A1: for X being ManySortedSet of I st X in A holds
X (/\) B = EmptyMS I ; :: thesis: (union A) (/\) B = EmptyMS I

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

let i be object ; :: thesis: ( i in I implies ((union A) (/\) B) . i = (EmptyMS I) . i )
assume A2: i in I ; :: thesis: ((union A) (/\) B) . i = (EmptyMS I) . i
for X9 being set st X9 in A . i holds
X9 misses B . i

proof

consider M being ManySortedSet of I such that
A3: M in A by PBOOLE:134;
let X9 be set ; :: thesis: ( X9 in A . i implies X9 misses B . i )
assume A4: X9 in A . i ; :: thesis: X9 misses B . i
dom (M +* (i .--> X9)) = I by A2, Lm1;
then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A5: dom (i .--> X9) = {i} ;
i in {i} by TARSKI:def 1;
then A6: K . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
K in A

proof

let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or K . j in A . j )
assume A7: j in I ; :: thesis: K . j in A . j

now :: thesis: ( ( j = i & K . j in A . j ) or ( j <> i & K . j in A . j ) )

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

case j = i ; :: thesis: K . j in A . j

hence K . j in A . j by A4, A6; :: thesis: verum

end;

case j <> i ; :: thesis: K . j in A . j

then not j in dom (i .--> X9) by TARSKI:def 1;
then K . j = M . j by FUNCT_4:11;
hence K . j in A . j by A3, A7; :: thesis: verum

end;

end;

end;

hence K . j in A . j ; :: thesis: verum

end;

then K (/\) B = EmptyMS I by A1;
then (K . i) /\ (B . i) = (EmptyMS I) . i by A2, PBOOLE:def 5;
then X9 /\ (B . i) = {} by A6, PBOOLE:5;
hence X9 misses B . i by XBOOLE_0:def 7; :: thesis: verum

end;

then union (A . i) misses B . i by ZFMISC_1:80;
then (union (A . i)) /\ (B . i) = {} by XBOOLE_0:def 7;
then ((union A) . i) /\ (B . i) = {} by A2, Def2;
then ((union A) (/\) B) . i = {} by A2, PBOOLE:def 5;
hence ((union A) (/\) B) . i = (EmptyMS I) . i by PBOOLE:5; :: thesis: verum

end;

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