let X be set ; :: thesis:
let S be cap-finite-partition-closed diff-c=-finite-partition-closed Subset-Family of X; :: thesis:
let SM be FinSequence of S; :: thesis:

suppose A0: S is empty ; :: thesis:

( {} is finite Subset of S & {} is a_partition of Union SM & ( for n being Nat st n in dom SM holds
SM . n = union { s where s is Element of S : ( s in {} & s c= SM . n ) } ) ) by A0, ZFMISC_1:2, EQREL_1:45;
hence ex P being finite Subset of S st
( P is a_partition of Union SM & ( for n being Nat st n in dom SM holds
SM . n = union { s where s is Element of S : ( s in P & s c= SM . n ) } ) ) ; :: thesis:

end;

suppose A1: not S is empty ; :: thesis:

defpred S₁[ object , object ] means ex A1 being set st
( A1 = $1 & A1 c= rng SM & $2 is finite Subset of S & $2 is a_partition of (meet A1) \ (union ((rng SM) \ A1)) );
set FFIN = { s where s is Subset of S : s c= rng SM } ;
set FFOUT = { s where s is finite Subset of S : ex K being set st
( K c= rng SM & s is a_partition of (meet K) \ (union ((rng SM) \ K)) ) } ;
A5: for x being object st x in { s where s is Subset of S : s c= rng SM } holds
ex y being object st
( y in { s where s is finite Subset of S : ex K being set st
( K c= rng SM & s is a_partition of (meet K) \ (union ((rng SM) \ K)) ) } & S₁[x,y] )

let x be object ; :: thesis:
assume x in { s where s is Subset of S : s c= rng SM } ; :: thesis:
then consider s0 being Subset of S such that
A6: ( x = s0 & s0 c= rng SM ) ;
consider PK being finite Subset of S such that
A7: PK is a_partition of (meet s0) \ (union ((rng SM) \ s0)) by A6, Thm3;
PK in { s where s is finite Subset of S : ex K being set st
( K c= rng SM & s is a_partition of (meet K) \ (union ((rng SM) \ K)) ) } by A6, A7;
hence ex y being object st
( y in { s where s is finite Subset of S : ex K being set st
( K c= rng SM & s is a_partition of (meet K) \ (union ((rng SM) \ K)) ) } & S₁[x,y] ) by A6, A7; :: thesis:

end;

consider ff being Function such that
A8: ( dom ff = { s where s is Subset of S : s c= rng SM } & rng ff c= { s where s is finite Subset of S : ex K being set st
( K c= rng SM & s is a_partition of (meet K) \ (union ((rng SM) \ K)) ) } ) and
A9: for x being object st x in { s where s is Subset of S : s c= rng SM } holds
S₁[x,ff . x] from FUNCT_1:sch 6(A5);
set FFALL = Union ff;
A10: for x being set st x in Union ff holds
ex x0 being set st
( x0 in dom ff & x in ff . x0 & x0 c= rng SM & ff . x0 is finite Subset of S & ff . x0 is a_partition of (meet x0) \ (union ((rng SM) \ x0)) )

let x be set ; :: thesis:
assume x in Union ff ; :: thesis:
then consider x0 being set such that
A11: ( x in x0 & x0 in rng ff ) by TARSKI:def 4;
consider a0 being object such that
A12: ( a0 in dom ff & x0 = ff . a0 ) by A11, FUNCT_1:def 3;
S₁[a0,ff . a0] by A8, A9, A12;
hence ex x0 being set st
( x0 in dom ff & x in ff . x0 & x0 c= rng SM & ff . x0 is finite Subset of S & ff . x0 is a_partition of (meet x0) \ (union ((rng SM) \ x0)) ) by A11, A12; :: thesis:

end;

A13: Union ff is finite Subset of S

A14: Union ff c= S

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union ff ; :: thesis:
then consider x0 being set such that
A15: ( x in x0 & x0 in rng ff ) by TARSKI:def 4;
consider a0 being object such that
A16: ( a0 in dom ff & x0 = ff . a0 ) by A15, FUNCT_1:def 3;
S₁[a0,ff . a0] by A8, A9, A16;
hence x in S by A15, A16; :: thesis:

end;

Union ff is finite

A18: { s where s is Subset of S : s c= rng SM } is finite

{ s where s is Subset of S : s c= rng SM } c= bool (rng SM)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { s where s is Subset of S : s c= rng SM } ; :: thesis:
then consider s0 being Subset of S such that
A19: ( x = s0 & s0 c= rng SM ) ;
thus x in bool (rng SM) by A19; :: thesis:

end;

hence { s where s is Subset of S : s c= rng SM } is finite ; :: thesis:

end;

Union ff is finite

for zz being set st zz in rng ff holds
zz is finite

let zz be set ; :: thesis:
assume zz in rng ff ; :: thesis:
then consider z0 being object such that
A20: ( z0 in { s where s is Subset of S : s c= rng SM } & zz = ff . z0 ) by A8, FUNCT_1:def 3;
S₁[z0,ff . z0] by A9, A20;
hence zz is finite by A20; :: thesis:

end;

hence Union ff is finite by A8, A18, FINSET_1:8, FINSET_1:7; :: thesis:

end;

hence Union ff is finite ; :: thesis:

end;

hence Union ff is finite Subset of S by A14; :: thesis:

end;

A21: for x being set st x in Union ff holds
x c= union (rng SM)

let x be set ; :: thesis:
assume x in Union ff ; :: thesis:
then consider x0 being set such that
A22: ( x in x0 & x0 in rng ff ) by TARSKI:def 4;
consider a0 being object such that
A23: ( a0 in dom ff & x0 = ff . a0 ) by A22, FUNCT_1:def 3;
reconsider a0 = a0 as set by TARSKI:1;
A24: S₁[a0,ff . a0] by A8, A9, A23;
(meet a0) \ (union ((rng SM) \ a0)) c= union (rng SM)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in (meet a0) \ (union ((rng SM) \ a0)) ; :: thesis:
x in Union SM

suppose a0 is empty ; :: thesis:

hence x in Union SM by A25, SETFAM_1:1; :: thesis:

end;

suppose not a0 is empty ; :: thesis:

then consider y0 being object such that
A26: y0 in a0 ;
reconsider y0 = y0 as set by TARSKI:1;
( x in y0 & y0 in rng SM ) by A24, A25, A26, SETFAM_1:def 1;
hence x in Union SM by TARSKI:def 4; :: thesis:

end;

end;

end;

hence x in union (rng SM) ; :: thesis:

end;

hence x c= union (rng SM) by A22, A23, A24, XBOOLE_1:1; :: thesis:

end;

A27: Union ff is a_partition of union (rng SM)

A28: Union ff c= bool (union (rng SM))

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume B01: x in Union ff ; :: thesis:
reconsider x = x as set by TARSKI:1;
x c= Union SM by B01, A21;
hence x in bool (union (rng SM)) ; :: thesis:

end;

A29: union (Union ff) = union (rng SM)

A30: union (Union ff) c= union (rng SM)

union (Union ff) c= union (bool (union (rng SM))) by A28, ZFMISC_1:77;
hence union (Union ff) c= union (rng SM) by ZFMISC_1:81; :: thesis:

end;

union (rng SM) c= union (Union ff)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A31: x in union (rng SM) ; :: thesis:
for x being set st x in union (rng SM) holds
ex aa being set st
( aa in dom ff & x in (meet aa) \ (union ((rng SM) \ aa)) )

let x be set ; :: thesis:
assume A32: x in union (rng SM) ; :: thesis:
defpred S₂[ FinSequence] means for x being set st x in union (rng $1) holds
ex aa being Subset of S st
( aa c= rng $1 & x in (meet aa) \ (union ((rng $1) \ aa)) );
A33: for p being FinSequence of S
for t being Element of S st S₂[p] holds
S₂[p ^ <*t*>]

let p be FinSequence of S; :: thesis:
let t be Element of S; :: thesis:
assume A34: S₂[p] ; :: thesis:
for x being set st x in union (rng (p ^ <*t*>)) holds
ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) )

let x be set ; :: thesis:
assume x in union (rng (p ^ <*t*>)) ; :: thesis:
then x in union ((rng p) \/ (rng <*t*>)) by FINSEQ_1:31;
then x in (Union p) \/ (Union <*t*>) by ZFMISC_1:78;
then A34a: x in (Union p) \/ (union {t}) by FINSEQ_1:38;
A36: ( x in Union p & x in t implies ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) )

assume A37: x in Union p ; :: thesis:
assume A38: x in t ; :: thesis:
consider aa1 being Subset of S such that
A39: ( aa1 c= rng p & x in (meet aa1) \ (union ((rng p) \ aa1)) ) by A34, A37;
set aa = aa1 \/ {t};
take aa1 \/ {t} ; :: thesis:
A40: ( {t} is Subset of S & aa1 is Subset of S ) by A1, SUBSET_1:33;
A41: aa1 \/ {t} c= rng (p ^ <*t*>)

rng (p ^ <*t*>) = (rng p) \/ (rng <*t*>) by FINSEQ_1:31;
then A42: rng (p ^ <*t*>) = (rng p) \/ {t} by FINSEQ_1:38;
A43: aa1 c= (rng p) \/ {t} by A39, XBOOLE_1:10;
{t} c= (rng p) \/ {t} by XBOOLE_1:7;
hence aa1 \/ {t} c= rng (p ^ <*t*>) by A42, A43, XBOOLE_1:8; :: thesis:

end;

( aa1 <> {} implies x in (meet (aa1 \/ {t})) \ (union ((rng (p ^ <*t*>)) \ (aa1 \/ {t}))) )

assume A44: aa1 <> {} ; :: thesis:
( x in meet aa1 & x in meet {t} ) by A38, A39, SETFAM_1:10;
then A45: x in (meet aa1) /\ (meet {t}) by XBOOLE_0:def 4;
A46: rng (p ^ <*t*>) = (rng p) \/ (rng <*t*>) by FINSEQ_1:31;
((rng p) \/ {t}) \ (aa1 \/ {t}) = ((rng p) \ (aa1 \/ {t})) \/ ({t} \ (aa1 \/ {t})) by XBOOLE_1:42;
then ((rng p) \/ {t}) \ (aa1 \/ {t}) = ((rng p) \ (aa1 \/ {t})) \/ {} by XBOOLE_1:46;
then (rng (p ^ <*t*>)) \ (aa1 \/ {t}) = (rng p) \ (aa1 \/ {t}) by A46, FINSEQ_1:38;
then (rng (p ^ <*t*>)) \ (aa1 \/ {t}) = ((rng p) \ aa1) /\ ((rng p) \ {t}) by XBOOLE_1:53;
then A47: union ((rng (p ^ <*t*>)) \ (aa1 \/ {t})) c= union ((rng p) \ aa1) by ZFMISC_1:77, XBOOLE_1:17;
( not x in union ((rng (p ^ <*t*>)) \ (aa1 \/ {t})) & x in meet (aa1 \/ {t}) ) by A39, A44, A45, A47, SETFAM_1:9, XBOOLE_0:def 5;
hence x in (meet (aa1 \/ {t})) \ (union ((rng (p ^ <*t*>)) \ (aa1 \/ {t}))) by XBOOLE_0:def 5; :: thesis:

end;

hence ( aa1 \/ {t} is Subset of S & aa1 \/ {t} c= rng (p ^ <*t*>) & x in (meet (aa1 \/ {t})) \ (union ((rng (p ^ <*t*>)) \ (aa1 \/ {t}))) ) by A39, A40, A41, XBOOLE_1:8, SETFAM_1:1; :: thesis:

end;

A48: ( x in Union p & not x in t implies ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) )

assume A49: x in Union p ; :: thesis:
assume A50: not x in t ; :: thesis:
consider aa1 being Subset of S such that
A51: ( aa1 c= rng p & x in (meet aa1) \ (union ((rng p) \ aa1)) ) by A34, A49;
set aa = aa1 \ {t};
A52: aa1 \ {t} c= rng (p ^ <*t*>)

A53: rng (p ^ <*t*>) = (rng p) \/ (rng <*t*>) by FINSEQ_1:31;
A54: aa1 c= (rng p) \/ {t} by A51, XBOOLE_1:10;
aa1 \ {t} c= aa1 by XBOOLE_1:36;
then aa1 \ {t} c= (rng p) \/ {t} by A54, XBOOLE_1:1;
hence aa1 \ {t} c= rng (p ^ <*t*>) by A53, FINSEQ_1:38; :: thesis:

end;

A55: ( aa1 <> {} & aa1 \ {t} = {} implies ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) )

assume A56: aa1 <> {} ; :: thesis:
assume aa1 \ {t} = {} ; :: thesis:
then A57: {t} = aa1 by A56, ZFMISC_1:58;
set aa = aa1;
A58: rng (p ^ <*t*>) = (rng p) \/ (rng <*t*>) by FINSEQ_1:31
.= (rng p) \/ {t} by FINSEQ_1:38 ;
A59: ((rng p) \/ {t}) \ {t} = (rng p) \ {t} by XBOOLE_1:40;
thus ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) by A51, A57, A58, A59, XBOOLE_1:11; :: thesis:

end;

( aa1 <> {} & aa1 \ {t} <> {} implies ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) )

assume aa1 <> {} ; :: thesis:
assume A60: aa1 \ {t} <> {} ; :: thesis:
A61: for y being set st y in aa1 holds
x in y \ t

let y be set ; :: thesis:
assume y in aa1 ; :: thesis:
then ( x in y & not x in t ) by A50, A51, SETFAM_1:def 1;
hence x in y \ t by XBOOLE_0:def 5; :: thesis:

end;

for y being set st y in aa1 \ {t} holds
x in y

let y be set ; :: thesis:
assume y in aa1 \ {t} ; :: thesis:
then ( y in aa1 & not y in {t} ) by XBOOLE_0:def 5;
then ( x in y \ t & not y = t ) by A61, TARSKI:def 1;
hence x in y ; :: thesis:

end;

then A62: x in meet (aa1 \ {t}) by A60, SETFAM_1:def 1;
rng (p ^ <*t*>) = (rng p) \/ (rng <*t*>) by FINSEQ_1:31;
then A63: (rng (p ^ <*t*>)) \ (aa1 \ {t}) = ((rng p) \/ {t}) \ (aa1 \ {t}) by FINSEQ_1:38;
A64: ({t} \ aa1) \/ {t} = {t} by XBOOLE_1:7, XBOOLE_1:8;
(rng (p ^ <*t*>)) \ (aa1 \ {t}) = ((rng p) \ (aa1 \ {t})) \/ ({t} \ (aa1 \ {t})) by A63, XBOOLE_1:42
.= ((rng p) \ (aa1 \ {t})) \/ (({t} \ aa1) \/ ({t} /\ {t})) by XBOOLE_1:52
.= (((rng p) \ aa1) \/ ((rng p) /\ {t})) \/ {t} by A64, XBOOLE_1:52
.= ((rng p) \ aa1) \/ (((rng p) /\ {t}) \/ {t}) by XBOOLE_1:4
.= ((rng p) \ aa1) \/ {t} by XBOOLE_1:22 ;
then A66: union ((rng (p ^ <*t*>)) \ (aa1 \ {t})) = (union ((rng p) \ aa1)) \/ (union {t}) by ZFMISC_1:78
.= (union ((rng p) \ aa1)) \/ t ;
A67: ( not x in t & not x in union ((rng p) \ aa1) implies not x in union ((rng (p ^ <*t*>)) \ (aa1 \ {t})) ) by A66, XBOOLE_0:def 3;
x in (meet (aa1 \ {t})) \ (union ((rng (p ^ <*t*>)) \ (aa1 \ {t}))) by A50, A51, A62, A67, XBOOLE_0:def 5;
hence ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) by A52; :: thesis:

end;

then consider aa being Subset of S such that
A68: ( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) by A51, A55, SETFAM_1:1;
thus ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) by A68; :: thesis:

end;

( not x in Union p & x in t implies ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) )

assume A69: not x in Union p ; :: thesis:
assume A70: x in t ; :: thesis:
A71: rng (p ^ <*t*>) = (rng p) \/ (rng <*t*>) by FINSEQ_1:31
.= (rng p) \/ {t} by FINSEQ_1:38 ;
set aa = {t} \ (rng p);
A72: {t} \ (rng p) is Subset of S

( {t} is Subset of S & rng p is Subset of S ) by A1, SUBSET_1:33;
hence {t} \ (rng p) is Subset of S by XBOOLE_1:1; :: thesis:

end;

x in (meet ({t} \ (rng p))) \ (union ((rng (p ^ <*t*>)) \ ({t} \ (rng p))))

A73: x in meet ({t} \ (rng p))

per cases \ (rng p) <> {} or {t} \ (rng p) = {} ) ;

suppose A74: {t} \ (rng p) <> {} ; :: thesis:

for y being set st y in {t} \ (rng p) holds
x in y by A70, TARSKI:def 1;
hence x in meet ({t} \ (rng p)) by A74, SETFAM_1:def 1; :: thesis:

end;

suppose {t} \ (rng p) = {} ; :: thesis:

then {t} is Subset of (rng p) by SUBSET_1:41, ZFMISC_1:60;
then union {t} c= Union p by ZFMISC_1:77;
hence x in meet ({t} \ (rng p)) by A69, A70; :: thesis:

end;

end;

end;

not x in union ((rng (p ^ <*t*>)) \ ({t} \ (rng p))) by A69, A71, Lem1;
hence x in (meet ({t} \ (rng p))) \ (union ((rng (p ^ <*t*>)) \ ({t} \ (rng p)))) by A73, XBOOLE_0:def 5; :: thesis:

end;

hence ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) by A72, A71, XBOOLE_1:10; :: thesis:

end;

hence ex aa being Subset of S st
( aa c= rng (p ^ <*t*>) & x in (meet aa) \ (union ((rng (p ^ <*t*>)) \ aa)) ) by A34a, A36, A48, XBOOLE_0:def 3; :: thesis:

end;

hence S₂[p ^ <*t*>] ; :: thesis:

end;

A75: S₂[ <*> S] by ZFMISC_1:2;
for p being FinSequence of S holds S₂[p] from FINSEQ_2:sch 2(A75, A33);
then consider aa being Subset of S such that
A76: ( aa c= rng SM & x in (meet aa) \ (union ((rng SM) \ aa)) ) by A32;
take aa ; :: thesis:
thus ( aa in dom ff & x in (meet aa) \ (union ((rng SM) \ aa)) ) by A8, A76; :: thesis:

end;

then consider aa being set such that
A77: ( aa in dom ff & x in (meet aa) \ (union ((rng SM) \ aa)) ) by A31;
S₁[aa,ff . aa] by A8, A9, A77;
then A78: x in union (ff . aa) by A77, EQREL_1:def 4;
ff . aa c= Union ff

let x be object ; :: according to TARSKI:def 3 :: thesis:
ff . aa in rng ff by A77, FUNCT_1:def 3;
hence ( not x in ff . aa or x in Union ff ) by TARSKI:def 4; :: thesis:

end;

then union (ff . aa) c= union (Union ff) by ZFMISC_1:77;
hence x in union (Union ff) by A78; :: thesis:

end;

hence union (Union ff) = union (rng SM) by A30; :: thesis:

end;

for A being Subset of (union (rng SM)) st A in Union ff holds
( A <> {} & ( for B being Subset of (union (rng SM)) holds
( not B in Union ff or A = B or A misses B ) ) )

let A be Subset of (union (rng SM)); :: thesis:
assume A80: A in Union ff ; :: thesis:
consider a0 being set such that
A81: ( a0 in dom ff & A in ff . a0 & a0 c= rng SM & ff . a0 is finite Subset of S & ff . a0 is a_partition of (meet a0) \ (union ((rng SM) \ a0)) ) by A10, A80;
for B being Subset of (union (rng SM)) holds
( not B in Union ff or A = B or A misses B )

let B be Subset of (union (rng SM)); :: thesis:
assume A82: B in Union ff ; :: thesis:
consider b0 being set such that
A83: ( b0 in dom ff & B in ff . b0 & b0 c= rng SM & ff . b0 is finite Subset of S & ff . b0 is a_partition of (meet b0) \ (union ((rng SM) \ b0)) ) by A10, A82;
A84: ( a0 <> b0 implies (meet b0) \ (union ((rng SM) \ b0)) misses (meet a0) \ (union ((rng SM) \ a0)) )

assume A85: a0 <> b0 ; :: thesis:
((meet b0) \ (union ((rng SM) \ b0))) /\ ((meet a0) \ (union ((rng SM) \ a0))) c= {}

let q be object ; :: according to TARSKI:def 3 :: thesis:
assume A87: q in ((meet b0) \ (union ((rng SM) \ b0))) /\ ((meet a0) \ (union ((rng SM) \ a0))) ; :: thesis:
A88: ( q in (meet b0) \ (union ((rng SM) \ b0)) & q in (meet a0) \ (union ((rng SM) \ a0)) ) by A87, XBOOLE_0:def 4;
then A89: ( q in meet b0 & not q in union ((rng SM) \ b0) & q in meet a0 & not q in union ((rng SM) \ a0) ) by XBOOLE_0:def 5;
A90: ( not a0 c= b0 implies q in {} )

assume not a0 c= b0 ; :: thesis:
then consider y0 being object such that
A91: ( y0 in a0 & not y0 in b0 ) by TARSKI:def 3;
reconsider y0 = y0 as set by TARSKI:1;
A92: q in y0 by A87, A91, SETFAM_1:def 1;
y0 in (rng SM) \ b0 by A81, A91, XBOOLE_0:def 5;
hence q in {} by A89, A92, TARSKI:def 4; :: thesis:

end;

( not b0 c= a0 implies q in {} )

assume not b0 c= a0 ; :: thesis:
then consider y0 being object such that
A99: ( y0 in b0 & not y0 in a0 ) by TARSKI:def 3;
reconsider y0 = y0 as set by TARSKI:1;
A100: q in y0 by A88, A99, SETFAM_1:def 1;
y0 in (rng SM) \ a0 by A83, A99, XBOOLE_0:def 5;
hence q in {} by A89, A100, TARSKI:def 4; :: thesis:

end;

hence q in {} by A85, A90; :: thesis:

end;

hence (meet b0) \ (union ((rng SM) \ b0)) misses (meet a0) \ (union ((rng SM) \ a0)) ; :: thesis:

end;

thus ( A = B or A misses B ) by A81, A83, A84, EQREL_1:def 4, XBOOLE_1:64; :: thesis:

end;

hence ( A <> {} & ( for B being Subset of (union (rng SM)) holds
( not B in Union ff or A = B or A misses B ) ) ) by A81; :: thesis:

end;

hence Union ff is a_partition of union (rng SM) by A28, A29, EQREL_1:def 4; :: thesis:

end;

for n being Nat st n in dom SM holds
SM . n = union { s where s is Element of S : ( s in Union ff & s c= SM . n ) }

let n be Nat; :: thesis:
assume A101: n in dom SM ; :: thesis:
A102: SM . n c= union { s where s is Element of S : ( s in Union ff & s c= SM . n ) }

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A103: x in SM . n ; :: thesis:
A104: union (Union ff) = union (rng SM) by A27, EQREL_1:def 4;
( x in SM . n & SM . n in rng SM ) by A101, A103, FUNCT_1:def 3;
then A105: x in union (rng SM) by TARSKI:def 4;
consider y0 being set such that
A106: ( x in y0 & y0 in Union ff ) by A104, A105, TARSKI:def 4;
consider d0 being set such that
A107: ( d0 in dom ff & y0 in ff . d0 & d0 c= rng SM & ff . d0 is finite Subset of S & ff . d0 is a_partition of (meet d0) \ (union ((rng SM) \ d0)) ) by A10, A106;
y0 c= SM . n

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in y0 ; :: thesis:
then A108: u in (meet d0) \ (union ((rng SM) \ d0)) by A107;
A109: ( {(SM . n)} c= d0 implies u in SM . n )

assume A110: {(SM . n)} c= d0 ; :: thesis:
A111: SM . n in {(SM . n)} by TARSKI:def 1;
thus u in SM . n by A108, A110, A111, SETFAM_1:def 1; :: thesis:

end;

( not {(SM . n)} c= d0 implies u in SM . n )

assume not {(SM . n)} c= d0 ; :: thesis:
then consider yy being object such that
A112: ( yy in {(SM . n)} & not yy in d0 ) by TARSKI:def 3;
( SM . n in rng SM & not SM . n in d0 ) by A101, A112, FUNCT_1:def 3, TARSKI:def 1;
then SM . n in (rng SM) \ d0 by XBOOLE_0:def 5;
then x in union ((rng SM) \ d0) by A103, TARSKI:def 4;
hence u in SM . n by A106, A107, XBOOLE_0:def 5; :: thesis:

end;

hence u in SM . n by A109; :: thesis:

end;

then ( x in y0 & y0 in { s where s is Element of S : ( s in Union ff & s c= SM . n ) } ) by A106, A107;
hence x in union { s where s is Element of S : ( s in Union ff & s c= SM . n ) } by TARSKI:def 4; :: thesis:

end;

union { s where s is Element of S : ( s in Union ff & s c= SM . n ) } c= SM . n

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union { s where s is Element of S : ( s in Union ff & s c= SM . n ) } ; :: thesis:
then consider y being set such that
A113: ( x in y & y in { s where s is Element of S : ( s in Union ff & s c= SM . n ) } ) by TARSKI:def 4;
consider s0 being Element of S such that
A114: ( y = s0 & s0 in Union ff & s0 c= SM . n ) by A113;
thus x in SM . n by A113, A114; :: thesis:

end;

hence SM . n = union { s where s is Element of S : ( s in Union ff & s c= SM . n ) } by A102; :: thesis:

end;

hence ex P being finite Subset of S st
( P is a_partition of Union SM & ( for n being Nat st n in dom SM holds
SM . n = union { s where s is Element of S : ( s in P & s c= SM . n ) } ) ) by A13, A27; :: thesis:

end;

end;