let X be set ; :: thesis:
let S be cap-finite-partition-closed Subset-Family of X; :: thesis:
let A, B be finite Subset of S; :: thesis:
assume that
A1: A is mutually-disjoint and
A2: B is mutually-disjoint ; :: thesis:

per cases <> {} or [:A,B:] = {} ) ;

suppose A3: [:A,B:] <> {} ; :: thesis:

defpred S₁[ object , object ] means ex a, b being set st
( a in A & b in B & $1 = [a,b] & ex p being finite Subset of S st
( p is a_partition of a /\ b & $2 = p ) );
set XIN = { s where s is Element of [:A,B:] : verum } ;
set XOUT = { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } ;
A4: for x being object st x in { s where s is Element of [:A,B:] : verum } holds
ex y being object st
( y in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } & S₁[x,y] )

proof

let x be object ; :: thesis:
assume x in { s where s is Element of [:A,B:] : verum } ; :: thesis:
then consider s being Element of [:A,B:] such that
A5: x = s ;
consider a0, b0 being object such that
A6: ( a0 in A & b0 in B ) and
A7: s = [a0,b0] by A3, ZFMISC_1:def 2;
reconsider a0 = a0, b0 = b0 as set by TARSKI:1;

per cases ;

suppose not a0 /\ b0 is empty ; :: thesis:

then consider P being finite Subset of S such that
A8: P is a_partition of a0 /\ b0 by A6, Defcap;
P in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } by A6, A8;
hence ex y being object st
( y in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } & S₁[x,y] ) by A5, A6, A7, A8; :: thesis:

end;

suppose a0 /\ b0 is empty ; :: thesis:

then A9: ( {} is finite Subset of S & {} is a_partition of a0 /\ b0 ) by SUBSET_1:1, EQREL_1:45;
then {} in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } by A6;
hence ex y being object st
( y in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } & S₁[x,y] ) by A5, A6, A7, A9; :: thesis:

end;

consider f being Function such that
A10: ( dom f = { s where s is Element of [:A,B:] : verum } & rng f c= { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } ) and
A11: for x being object st x in { s where s is Element of [:A,B:] : verum } holds
S₁[x,f . x] from FUNCT_1:sch 6(A4);
A12: Union f is finite

proof

A13: [:A,B:] = { s where s is Element of [:A,B:] : verum }

proof

A14: [:A,B:] c= { s where s is Element of [:A,B:] : verum }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in [:A,B:] ; :: thesis:
hence x in { s where s is Element of [:A,B:] : verum } ; :: thesis:

end;

{ s where s is Element of [:A,B:] : verum } c= [:A,B:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { s where s is Element of [:A,B:] : verum } ; :: thesis:
then consider s being Element of [:A,B:] such that
A15: s = x ;
thus x in [:A,B:] by A3, A15; :: thesis:

end;

hence [:A,B:] = { s where s is Element of [:A,B:] : verum } by A14; :: thesis:

end;

for z being set st z in rng f holds
z is finite

proof

let z be set ; :: thesis:
assume z in rng f ; :: thesis:
then z in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } by A10;
then consider s0 being finite Subset of S such that
A16: s0 = z and
ex a, b being set st
( a in A & b in B & s0 is a_partition of a /\ b ) ;
thus z is finite by A16; :: thesis:

end;

hence Union f is finite by A13, A10, FINSET_1:8, FINSET_1:7; :: thesis:

end;

A17: Union f c= S

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union f ; :: thesis:
then consider y being set such that
A18: ( x in y & y in rng f ) by TARSKI:def 4;
y in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } by A18, A10;
then consider s0 being finite Subset of S such that
A19: y = s0 and
ex a, b being set st
( a in A & b in B & s0 is a_partition of a /\ b ) ;
thus x in S by A18, A19; :: thesis:

end;

A20: Union f c= bool ((union A) /\ (union B))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union f ; :: thesis:
then consider y being set such that
A21: x in y and
A22: y in rng f by TARSKI:def 4;
y in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } by A22, A10;
then consider s0 being finite Subset of S such that
A23: y = s0 and
A24: ex a, b being set st
( a in A & b in B & s0 is a_partition of a /\ b ) ;
reconsider x = x as set by TARSKI:1;
consider a0, b0 being set such that
A25: ( a0 in A & b0 in B ) and
A26: s0 is a_partition of a0 /\ b0 by A24;
( a0 c= union A & b0 c= union B ) by A25, ZFMISC_1:74;
then a0 /\ b0 c= (union A) /\ (union B) by XBOOLE_1:27;
then x c= (union A) /\ (union B) by XBOOLE_1:1, A21, A23, A26;
hence x in bool ((union A) /\ (union B)) ; :: thesis:

end;

A27: union (Union f) = (union A) /\ (union B)

proof

A28: union (Union f) c= (union A) /\ (union B)

proof

union (Union f) c= union (bool ((union A) /\ (union B))) by A20, ZFMISC_1:77;
hence union (Union f) c= (union A) /\ (union B) by ZFMISC_1:81; :: thesis:

end;

(union A) /\ (union B) c= union (Union f)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (union A) /\ (union B) ; :: thesis:
then A29: ( x in union A & x in union B ) by XBOOLE_0:def 4;
then consider a being set such that
A30: ( x in a & a in A ) by TARSKI:def 4;
consider b being set such that
A31: ( x in b & b in B ) by A29, TARSKI:def 4;
[a,b] in [:A,B:] by A30, A31, ZFMISC_1:def 2;
then A32: [a,b] in { s where s is Element of [:A,B:] : verum } ;
then S₁[[a,b],f . [a,b]] by A11;
then consider a0, b0 being set such that
( a0 in A & b0 in B ) and
A33: [a,b] = [a0,b0] and
A34: ex p being finite Subset of S st
( p is a_partition of a0 /\ b0 & f . [a0,b0] = p ) ;
consider p being finite Subset of S such that
A35: p is a_partition of a0 /\ b0 and
A36: f . [a0,b0] = p by A34;
A37: ( a0 = a & b0 = b ) by A33, XTUPLE_0:1;
f . [a,b] in rng f by A32, A10, FUNCT_1:def 3;
then A38: union (f . [a,b]) c= union (union (rng f)) by ZFMISC_1:77, ZFMISC_1:74;
x in a /\ b by A30, A31, XBOOLE_0:def 4;
then x in union (f . [a,b]) by A35, A36, A37, EQREL_1:def 4;
hence x in union (Union f) by A38; :: thesis:

end;

hence union (Union f) = (union A) /\ (union B) by A28; :: thesis:

end;

for u being Subset of ((union A) /\ (union B)) st u in Union f holds
( u <> {} & ( for v being Subset of ((union A) /\ (union B)) holds
( not v in Union f or u = v or u misses v ) ) )

proof

let u be Subset of ((union A) /\ (union B)); :: thesis:
assume u in Union f ; :: thesis:
then consider v being set such that
A39: u in v and
A40: v in rng f by TARSKI:def 4;
consider w being object such that
A41: w in dom f and
A42: v = f . w by A40, FUNCT_1:def 3;
consider x being Element of [:A,B:] such that
A43: w = x by A41, A10;
reconsider w = w as Element of [:A,B:] by A43;
consider wa, wb being object such that
( wa in A & wb in B ) and
A44: w = [wa,wb] by A3, ZFMISC_1:def 2;
consider a, b being set such that
A45: ( a in A & b in B ) and
A46: [wa,wb] = [a,b] and
A47: ex p being finite Subset of S st
( p is a_partition of a /\ b & f . w = p ) by A41, A10, A11, A44;
consider p being finite Subset of S such that
A48: p is a_partition of a /\ b and
A49: f . w = p by A47;
v in { s where s is finite Subset of S : ex a, b being set st
( a in A & b in B & s is a_partition of a /\ b ) } by A40, A10;
then consider s0 being finite Subset of S such that
A50: v = s0 and
A51: ex a, b being set st
( a in A & b in B & s0 is a_partition of a /\ b ) ;
consider a0, b0 being set such that
( a0 in A & b0 in B ) and
A52: s0 is a_partition of a0 /\ b0 by A51;
thus u <> {} by A39, A50, A52; :: thesis:
thus for v being Subset of ((union A) /\ (union B)) holds
( not v in Union f or u = v or u misses v ) :: thesis:

proof

let jw be Subset of ((union A) /\ (union B)); :: thesis:
assume jw in Union f ; :: thesis:
then consider lw0 being set such that
A53: jw in lw0 and
A54: lw0 in rng f by TARSKI:def 4;
consider lw being object such that
A55: lw in dom f and
A56: lw0 = f . lw by A54, FUNCT_1:def 3;
consider lx being Element of [:A,B:] such that
A57: lw = lx by A55, A10;
reconsider lw = lw as Element of [:A,B:] by A57;
consider lwa, lwb being object such that
( lwa in A & lwb in B ) and
A58: lw = [lwa,lwb] by A3, ZFMISC_1:def 2;
consider la, lb being set such that
A59: ( la in A & lb in B ) and
A60: [lwa,lwb] = [la,lb] and
A61: ex p being finite Subset of S st
( p is a_partition of la /\ lb & f . lw = p ) by A55, A10, A11, A58;
consider lp being finite Subset of S such that
A62: lp is a_partition of la /\ lb and
A63: f . lw = lp by A61;

per cases ;

suppose ( a = la & b = lb ) ; :: thesis:

hence ( u = jw or u misses jw ) by A39, A42, A44, A46, A56, A58, A60, A63, A62, A53, EQREL_1:def 4; :: thesis:

end;

suppose A64: ( a <> la or b <> lb ) ; :: thesis:

( a /\ b c= b & la /\ lb c= lb & a /\ b c= a & la /\ lb c= la ) by XBOOLE_1:17;
then a /\ b misses la /\ lb by A64, A45, A59, A1, A2, TAXONOM2:def 5, XBOOLE_1:64;
hence ( u = jw or u misses jw ) by A39, A49, A48, A42, A56, A63, A62, A53, XBOOLE_1:64; :: thesis:

end;

then Union f is a_partition of (union A) /\ (union B) by A20, A27, EQREL_1:def 4;
hence ex P being finite Subset of S st P is a_partition of (union A) /\ (union B) by A12, A17; :: thesis:

end;

suppose [:A,B:] = {} ; :: thesis:

then ( A = {} or B = {} ) ;
hence ex P being finite Subset of S st P is a_partition of (union A) /\ (union B) by ZFMISC_1:2, EQREL_1:45; :: thesis:

end;