let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for A, B being set st A in S & B in DisUnion S holds
B \ A in DisUnion S
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for A, B being set st A in S & B in DisUnion S holds
B \ A in DisUnion S
let A, B be set ; :: thesis: ( A in S & B in DisUnion S implies B \ A in DisUnion S )
assume A2: ( A in S & B in DisUnion S ) ; :: thesis: B \ A in DisUnion S
reconsider A1 = A as Subset of X by A2;
consider B1 being Subset of X such that
A5: ( B = B1 & ex F being disjoint_valued FinSequence of S st B1 = Union F ) by A2;
consider g1 being disjoint_valued FinSequence of S such that
A6: B1 = Union g1 by A5;
reconsider R1 = DisUnion S as non empty set ;
defpred S₁[ Nat, object ] means $2 = (g1 . $1) \ A1;
A7: for k being Nat st k in Seg (len g1) holds
ex x being Element of R1 st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len g1) implies ex x being Element of R1 st S₁[k,x] )
assume k in Seg (len g1) ; :: thesis: ex x being Element of R1 st S₁[k,x]
then k in dom g1 by FINSEQ_1:def 3;
then ( g1 . k in rng g1 & rng g1 c= S ) by FUNCT_1:3;
then (g1 . k) \ A1 in DisUnion S by A2, lemma103;
hence ex x being Element of R1 st S₁[k,x] ; :: thesis: verum

end;

consider g2 being FinSequence of R1 such that
A8: ( dom g2 = Seg (len g1) & ( for k being Nat st k in Seg (len g1) holds
S₁[k,g2 . k] ) ) from FINSEQ_1:sch 5(A7);
A11: for n, m being Nat st n in dom g2 & m in dom g2 & n <> m holds
g2 . n misses g2 . m

proof

let n, m be Nat; :: thesis: ( n in dom g2 & m in dom g2 & n <> m implies g2 . n misses g2 . m )
assume A9: ( n in dom g2 & m in dom g2 & n <> m ) ; :: thesis: g2 . n misses g2 . m
then A10: ( g2 . n = (g1 . n) \ A1 & g2 . m = (g1 . m) \ A1 ) by A8;
g1 . n misses g2 . m by A10, A9, PROB_2:def 2, XBOOLE_1:80;
hence g2 . n misses g2 . m by A10, XBOOLE_1:80; :: thesis: verum

end;

set R = DisUnion S;
defpred S₂[ Nat] means union (rng (g2 | $1)) in DisUnion S;
( union (rng (g2 | 0)) in S & S c= DisUnion S ) by lemma100, SETFAM_1:def 8, ZFMISC_1:2;
then A12: S₂[ 0 ] ;
A13: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A14: S₂[k] ; :: thesis: S₂[k + 1]

per cases ( k + 1 <= len g2 or k + 1 > len g2 ) ;

suppose A15: k + 1 <= len g2 ; :: thesis: S₂[k + 1]

then A20: ( k <= len g2 & k <= k + 1 ) by NAT_1:13;
then ( len (g2 | (k + 1)) = k + 1 & g2 | k = (g2 | (k + 1)) | k ) by A15, FINSEQ_1:59, FINSEQ_1:82;
then g2 | (k + 1) = (g2 | k) ^ <*((g2 | (k + 1)) . (k + 1))*> by FINSEQ_3:55;
then rng (g2 | (k + 1)) = (rng (g2 | k)) \/ (rng <*((g2 | (k + 1)) . (k + 1))*>) by FINSEQ_1:31
.= (rng (g2 | k)) \/ {((g2 | (k + 1)) . (k + 1))} by FINSEQ_1:38
.= (rng (g2 | k)) \/ {(g2 . (k + 1))} by FINSEQ_3:112 ;
then A16: union (rng (g2 | (k + 1))) = (union (rng (g2 | k))) \/ (union {(g2 . (k + 1))}) by ZFMISC_1:78
.= (union (rng (g2 | k))) \/ (g2 . (k + 1)) ;
A24: k + 1 in dom g2 by A15, FINSEQ_3:25, NAT_1:11;

A25: now :: thesis: not union (rng (g2 | k)) meets g2 . (k + 1)

assume union (rng (g2 | k)) meets g2 . (k + 1) ; :: thesis: contradiction
then consider x being object such that
A17: ( x in union (rng (g2 | k)) & x in g2 . (k + 1) ) by XBOOLE_0:3;
consider Z being set such that
A18: ( x in Z & Z in rng (g2 | k) ) by A17, TARSKI:def 4;
consider i being object such that
A19: ( i in dom (g2 | k) & Z = (g2 | k) . i ) by A18, FUNCT_1:def 3;
reconsider i = i as Nat by A19;
i <= len (g2 | k) by A19, FINSEQ_3:25;
then A21: i <= k by A20, FINSEQ_1:59;
then A22: Z = g2 . i by A19, FINSEQ_3:112;
A23: dom (g2 | k) c= dom g2 by RELAT_1:60;
i <> k + 1 by A21, NAT_1:13;
then Z misses g2 . (k + 1) by A11, A22, A23, A19, A24;
hence contradiction by A17, A18, XBOOLE_0:def 4; :: thesis: verum

end;

( g2 . (k + 1) in rng g2 & rng g2 c= DisUnion S ) by A24, FUNCT_1:3;
hence union (rng (g2 | (k + 1))) in DisUnion S by A14, A16, A25, lemma102; :: thesis: verum

end;

suppose k + 1 > len g2 ; :: thesis: S₂[k + 1]

then ( g2 | (k + 1) = g2 & g2 | k = g2 ) by FINSEQ_1:58, NAT_1:13;
hence union (rng (g2 | (k + 1))) in DisUnion S by A14; :: thesis: verum

end;

end;

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A12, A13);
then C1: S₂[ len g2] ;

now :: thesis: for x being object st x in union (rng g2) holds
x in (union (rng g1)) \ A1

let x be object ; :: thesis: ( x in union (rng g2) implies x in (union (rng g1)) \ A1 )
assume x in union (rng g2) ; :: thesis: x in (union (rng g1)) \ A1
then consider y being set such that
B1: ( x in y & y in rng g2 ) by TARSKI:def 4;
consider k being object such that
B2: ( k in dom g2 & y = g2 . k ) by B1, FUNCT_1:def 3;
reconsider k = k as Nat by B2;
C3: g2 . k = (g1 . k) \ A1 by B2, A8;
then B3: ( x in g1 . k & not x in A1 ) by B1, B2, XBOOLE_0:def 5;
k in dom g1 by B2, A8, FINSEQ_1:def 3;
then g1 . k in rng g1 by FUNCT_1:3;
then x in union (rng g1) by C3, B1, B2, TARSKI:def 4;
hence x in (union (rng g1)) \ A1 by B3, XBOOLE_0:def 5; :: thesis: verum

end;

then B4: union (rng g2) c= (union (rng g1)) \ A1 ;

now :: thesis: for x being object st x in (union (rng g1)) \ A1 holds
x in union (rng g2)

let x be object ; :: thesis: ( x in (union (rng g1)) \ A1 implies x in union (rng g2) )
assume C5: x in (union (rng g1)) \ A1 ; :: thesis: x in union (rng g2)
then B5: ( x in union (rng g1) & not x in A1 ) by XBOOLE_0:def 5;
consider y being set such that
B6: ( x in y & y in rng g1 ) by C5, TARSKI:def 4;
consider k being object such that
B7: ( k in dom g1 & y = g1 . k ) by B6, FUNCT_1:def 3;
reconsider k = k as Nat by B7;
B8: k in dom g2 by B7, A8, FINSEQ_1:def 3;
then g2 . k = (g1 . k) \ A1 by A8;
then ( x in g2 . k & g2 . k in rng g2 ) by B5, B6, B7, B8, XBOOLE_0:def 5, FUNCT_1:3;
hence x in union (rng g2) by TARSKI:def 4; :: thesis: verum

end;

then (union (rng g1)) \ A1 c= union (rng g2) ;
then (union (rng g1)) \ A1 = union (rng g2) by B4;
hence B \ A in DisUnion S by A5, A6, C1, FINSEQ_1:58; :: thesis: verum