let X be set ; :: thesis:
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis:
let F be FinSequence of S; :: thesis:
let G be Element of S; :: thesis:
defpred S₁[ Nat] means for f being FinSequence of S st len f = $1 holds
ex H being disjoint_valued FinSequence of S st G \ (Union f) = Union H;
for f being FinSequence of S st len f = 0 holds
ex H being disjoint_valued FinSequence of S st G \ (Union f) = Union H

proof

let f be FinSequence of S; :: thesis:
assume len f = 0 ; :: thesis:
then f = {} ;
then rng f = {} ;
then A4: Union f = {} by CARD_3:def 4, ZFMISC_1:2;
A5: rng <*G*> = {G} by FINSEQ_1:38;
reconsider H = <*G*> as disjoint_valued FinSequence of S ;
take H ; :: thesis:
union (rng H) = G by A5, ZFMISC_1:25;
hence G \ (Union f) = Union H by A4, CARD_3:def 4; :: thesis:

end;

then A6: S₁[ 0 ] ;
A7: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A8: S₁[i] ; :: thesis:

now :: thesis:

let f be FinSequence of S; :: thesis:
assume A9: len f = i + 1 ; :: thesis:
then len (f | i) = i by NAT_1:11, FINSEQ_1:59;
then consider h being disjoint_valued FinSequence of S such that
A12: G \ (Union (f | i)) = Union h by A8;
A10: f = (f | i) ^ <*(f . (i + 1))*> by A9, FINSEQ_3:55;
then reconsider f1 = <*(f . (i + 1))*> as FinSequence of S by FINSEQ_1:36;
A11: Union f1 = union (rng f1) by CARD_3:def 4
.= union {(f . (i + 1))} by FINSEQ_1:38
.= f . (i + 1) by ZFMISC_1:25 ;
Union f = (Union (f | i)) \/ (Union f1) by A10, ROUGHS_1:5;
then A13: G \ (Union f) = (G \ (Union (f | i))) \ (f . (i + 1)) by A11, XBOOLE_1:41
.= (Union h) \ (f . (i + 1)) by A12 ;
deffunc H₁( Nat) -> Element of bool (h . $1) = (h . $1) \ (f . (i + 1));
consider V being FinSequence such that
A14: ( len V = len h & ( for k being Nat st k in dom V holds
V . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A19: for k being Nat st k in dom V holds
ex D being disjoint_valued FinSequence of S st V . k = Union D

proof

let k be Nat; :: thesis:
assume A15: k in dom V ; :: thesis:
k in dom h by A14, A15, FINSEQ_3:29;
then A16: h . k in rng h by FUNCT_1:3;
i + 1 in Seg (len f) by A9, FINSEQ_1:4;
then i + 1 in dom f by FINSEQ_1:def 3;
then f . (i + 1) in rng f by FUNCT_1:3;
then consider D being disjoint_valued FinSequence of S such that
A18: (h . k) \ (f . (i + 1)) = Union D by A16, SRINGS_3:def 1;
take D ; :: thesis:
thus V . k = Union D by A15, A14, A18; :: thesis:

end;

defpred S₂[ Nat, object ] means ex D being disjoint_valued FinSequence of S st
( $2 = D & V . $1 = Union D );
P1: for k being Nat st k in Seg (len V) holds
ex x being object st S₂[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len V) ; :: thesis:
then k in dom V by FINSEQ_1:def 3;
then consider D being disjoint_valued FinSequence of S such that
P2: V . k = Union D by A19;
take D ; :: thesis:
thus S₂[k,D] by P2; :: thesis:

end;

consider FinS being FinSequence such that
P3: ( dom FinS = Seg (len V) & ( for k being Nat st k in Seg (len V) holds
S₂[k,FinS . k] ) ) from FINSEQ_1:sch 1(P1);

now :: thesis:

let a be object ; :: thesis:
assume a in rng FinS ; :: thesis:
then consider x being object such that
P4: ( x in dom FinS & a = FinS . x ) by FUNCT_1:def 3;
consider D being disjoint_valued FinSequence of S such that
P5: ( FinS . x = D & V . x = Union D ) by P3, P4;
thus a is FinSequence of S by P4, P5; :: thesis:

end;

then reconsider Y = rng FinS as FinSequenceSet of S by FINSEQ_2:def 3;
reconsider FinS = FinS as FinSequence of Y by FINSEQ_1:def 4;
H1: for n, m being Nat st n <> m holds
union (rng (FinS . n)) misses union (rng (FinS . m))

proof

let n, m be Nat; :: thesis:
assume H2: n <> m ; :: thesis:

per cases ;

suppose H3: ( n in dom FinS & m in dom FinS ) ; :: thesis:

then consider D1 being disjoint_valued FinSequence of S such that
H4: ( FinS . n = D1 & V . n = Union D1 ) by P3;
consider D2 being disjoint_valued FinSequence of S such that
H5: ( FinS . m = D2 & V . m = Union D2 ) by H3, P3;
H6: ( V . n = union (rng (FinS . n)) & V . m = union (rng (FinS . m)) ) by H4, H5, CARD_3:def 4;
( n in dom V & m in dom V ) by H3, P3, FINSEQ_1:def 3;
then P15: ( V . n = (h . n) \ (f . (i + 1)) & V . m = (h . m) \ (f . (i + 1)) ) by A14;
then V . n misses h . m by XBOOLE_1:80, H2, PROB_2:def 2;
hence union (rng (FinS . n)) misses union (rng (FinS . m)) by H6, P15, XBOOLE_1:80; :: thesis:

end;

suppose ( not n in dom FinS or not m in dom FinS ) ; :: thesis:

then ( FinS . n = {} or FinS . m = {} ) by FUNCT_1:def 2;
then ( rng (FinS . n) = {} or rng (FinS . m) = {} ) ;
hence union (rng (FinS . n)) misses union (rng (FinS . m)) by ZFMISC_1:2, XBOOLE_1:65; :: thesis:

end;

for n being Nat holds FinS . n is disjoint_valued

proof

let n be Nat; :: thesis:

per cases ;

suppose not n in dom FinS ; :: thesis:

hence FinS . n is disjoint_valued by FUNCT_1:def 2; :: thesis:

end;

suppose n in dom FinS ; :: thesis:

then ex D being disjoint_valued FinSequence of S st
( FinS . n = D & V . n = Union D ) by P3;
hence FinS . n is disjoint_valued ; :: thesis:

end;

then reconsider H = joined_FinSeq FinS as disjoint_valued FinSequence of S by H1, Th14;
take H = H; :: thesis:
Union H = union (rng H) by CARD_3:def 4;
then X1: Union H = union (union { (rng (FinS . n)) where n is Nat : n in dom FinS } ) by Th15;
X2: G \ (Union f) = (union (rng h)) \ (f . (i + 1)) by CARD_3:def 4, A13;

now :: thesis:

let x be object ; :: thesis:
assume B0: x in (union (rng h)) \ (f . (i + 1)) ; :: thesis:
then consider A being set such that
B2: ( x in A & A in rng h ) by TARSKI:def 4;
consider k being object such that
B3: ( k in dom h & A = h . k ) by B2, FUNCT_1:def 3;
reconsider k = k as Nat by B3;
B4: k in dom V by A14, B3, FINSEQ_3:29;
B5: k in dom FinS by P3, FINSEQ_1:def 3, A14, B3;
then consider D being disjoint_valued FinSequence of S such that
B6: ( FinS . k = D & V . k = Union D ) by P3;
B7: V . k = union (rng (FinS . k)) by B6, CARD_3:def 4;
( x in union (rng h) & not x in f . (i + 1) ) by B0, XBOOLE_0:def 5;
then x in (h . k) \ (f . (i + 1)) by B2, B3, XBOOLE_0:def 5;
then x in V . k by A14, B4;
then consider V being set such that
B8: ( x in V & V in rng (FinS . k) ) by B7, TARSKI:def 4;
rng (FinS . k) in { (rng (FinS . n)) where n is Nat : n in dom FinS } by B5;
then V in union { (rng (FinS . n)) where n is Nat : n in dom FinS } by B8, TARSKI:def 4;
hence x in union (union { (rng (FinS . n)) where n is Nat : n in dom FinS } ) by B8, TARSKI:def 4; :: thesis:

end;

then B9: G \ (Union f) c= Union H by X1, X2, TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:
assume x in union (union { (rng (FinS . n)) where n is Nat : n in dom FinS } ) ; :: thesis:
then consider A being set such that
C1: ( x in A & A in union { (rng (FinS . n)) where n is Nat : n in dom FinS } ) by TARSKI:def 4;
consider D1 being set such that
C2: ( A in D1 & D1 in { (rng (FinS . n)) where n is Nat : n in dom FinS } ) by C1, TARSKI:def 4;
consider k being Nat such that
C3: ( D1 = rng (FinS . k) & k in dom FinS ) by C2;
consider D2 being disjoint_valued FinSequence of S such that
C4: ( FinS . k = D2 & V . k = Union D2 ) by C3, P3;
C5: k in dom V by C3, P3, FINSEQ_1:def 3;
then V . k = (h . k) \ (f . (i + 1)) by A14;
then (h . k) \ (f . (i + 1)) = union D1 by C3, C4, CARD_3:def 4;
then C6: x in (h . k) \ (f . (i + 1)) by C1, C2, TARSKI:def 4;
then C7: ( x in h . k & not x in f . (i + 1) ) by XBOOLE_0:def 5;
dom V = dom h by A14, FINSEQ_3:29;
then h . k in rng h by C5, FUNCT_1:3;
then x in union (rng h) by C6, TARSKI:def 4;
hence x in (union (rng h)) \ (f . (i + 1)) by C7, XBOOLE_0:def 5; :: thesis:

end;

then Union H c= G \ (Union f) by X1, X2, TARSKI:def 3;
hence G \ (Union f) = Union H by B9, XBOOLE_0:def 10; :: thesis:

end;

hence S₁[i + 1] ; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A7);
then for f being FinSequence of S st len f = len F holds
ex H being disjoint_valued FinSequence of S st G \ (Union f) = Union H ;
hence ex H being disjoint_valued FinSequence of S st G \ (Union F) = Union H ; :: thesis: