let X be set ; :: thesis: for f being SetSequence of X ex g being SetSequence of X st
( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )
let f be SetSequence of X; :: thesis: ex g being SetSequence of X st
( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )
defpred S₁[ set , set ] means for n being Nat st n = $1 holds
ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & $2 = (f . n) \ (union fn) );
A1: for x being set st x in NAT holds
ex y being set st
( y in bool X & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in bool X & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in bool X & S₁[x,y] )
then reconsider n = x as Element of NAT ;
deffunc H₁( Nat) -> Element of bool X = f . $1;
set fn = { H₁(i) where i is Element of NAT : i in n } ;
A2: { H₁(i) where i is Element of NAT : i in n } c= bool X

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { H₁(i) where i is Element of NAT : i in n } or z in bool X )
assume z in { H₁(i) where i is Element of NAT : i in n } ; :: thesis: z in bool X
then ex i being Element of NAT st
( z = H₁(i) & i in n ) ;
hence z in bool X ; :: thesis: verum

end;

A3: n is finite ;
{ H₁(i) where i is Element of NAT : i in n } is finite from FRAENKEL:sch 21(A3);
then reconsider fn = { H₁(i) where i is Element of NAT : i in n } as finite Subset-Family of X by A2;
take y = (f . n) \ (union fn); :: thesis: ( y in bool X & S₁[x,y] )
thus y in bool X ; :: thesis: S₁[x,y]
let m be Nat; :: thesis: ( m = x implies ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < m } & y = (f . m) \ (union fn) ) )
assume A4: m = x ; :: thesis: ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < m } & y = (f . m) \ (union fn) )
set Fn = { (f . i) where i is Element of NAT : i < n } ;
take fn ; :: thesis: ( fn = { (f . i) where i is Element of NAT : i < m } & y = (f . m) \ (union fn) )
A5: fn c= { (f . i) where i is Element of NAT : i < n }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in fn or z in { (f . i) where i is Element of NAT : i < n } )
assume z in fn ; :: thesis: z in { (f . i) where i is Element of NAT : i < n }
then consider i being Element of NAT such that
A6: z = f . i and
A7: i in n ;
i < n by A7, NAT_1:44;
hence z in { (f . i) where i is Element of NAT : i < n } by A6; :: thesis: verum

end;

{ (f . i) where i is Element of NAT : i < n } c= fn

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { (f . i) where i is Element of NAT : i < n } or z in fn )
assume z in { (f . i) where i is Element of NAT : i < n } ; :: thesis: z in fn
then consider i being Element of NAT such that
A8: z = f . i and
A9: i < n ;
i in n by A9, NAT_1:44;
hence z in fn by A8; :: thesis: verum

end;

hence ( fn = { (f . i) where i is Element of NAT : i < m } & y = (f . m) \ (union fn) ) by A4, A5, XBOOLE_0:def 10; :: thesis: verum

end;

consider g being SetSequence of X such that
A10: for x being set st x in NAT holds
S₁[x,g . x] from FUNCT_2:sch 1(A1);
take g ; :: thesis: ( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )
A11: union (rng f) c= union (rng g)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union (rng f) or y in union (rng g) )
defpred S₂[ Nat] means y in f . $1;
assume y in union (rng f) ; :: thesis: y in union (rng g)
then consider Y being set such that
A12: y in Y and
A13: Y in rng f by TARSKI:def 4;
ex x being set st
( x in dom f & f . x = Y ) by A13, FUNCT_1:def 3;
then A14: ex n being Nat st S₂[n] by A12;
consider Min being Nat such that
A15: S₂[Min] and
A16: for n being Nat st S₂[n] holds
Min <= n from NAT_1:sch 5(A14);
A17: Min in NAT by ORDINAL1:def 12;
then consider fn being finite Subset-Family of X such that
A18: fn = { (f . i) where i is Element of NAT : i < Min } and
A19: g . Min = (f . Min) \ (union fn) by A10;
not y in union fn

proof

assume y in union fn ; :: thesis: contradiction
then consider Z being set such that
A20: y in Z and
A21: Z in fn by TARSKI:def 4;
ex i being Element of NAT st
( Z = f . i & i < Min ) by A18, A21;
hence contradiction by A16, A20; :: thesis: verum

end;

then A22: y in g . Min by A15, A19, XBOOLE_0:def 5;
dom g = NAT by FUNCT_2:def 1;
then g . Min in rng g by A17, FUNCT_1:def 3;
hence y in union (rng g) by A22, TARSKI:def 4; :: thesis: verum

end;

union (rng g) c= union (rng f)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in union (rng g) or y in union (rng f) )
assume y in union (rng g) ; :: thesis: y in union (rng f)
then consider Y being set such that
A23: y in Y and
A24: Y in rng g by TARSKI:def 4;
consider x being set such that
A25: x in dom g and
A26: g . x = Y by A24, FUNCT_1:def 3;
reconsider n = x as Nat by A25;
ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) by A10, A25;
then A27: y in f . n by A23, A26, XBOOLE_0:def 5;
dom f = NAT by FUNCT_2:def 1;
then f . n in rng f by A25, FUNCT_1:def 3;
hence y in union (rng f) by A27, TARSKI:def 4; :: thesis: verum

end;

hence union (rng f) = union (rng g) by A11, XBOOLE_0:def 10; :: thesis: ( ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )
A28: for i, j being Nat st i < j holds
g . i misses g . j

proof

let i, j be Nat; :: thesis: ( i < j implies g . i misses g . j )
assume A29: i < j ; :: thesis: g . i misses g . j
j in NAT by ORDINAL1:def 12;
then consider fj being finite Subset-Family of X such that
A30: fj = { (f . n) where n is Element of NAT : n < j } and
A31: g . j = (f . j) \ (union fj) by A10;
assume g . i meets g . j ; :: thesis: contradiction
then consider x being set such that
A32: x in g . i and
A33: x in g . j by XBOOLE_0:3;
A34: i in NAT by ORDINAL1:def 12;
then ex fi being finite Subset-Family of X st
( fi = { (f . n) where n is Element of NAT : n < i } & g . i = (f . i) \ (union fi) ) by A10;
then A35: x in f . i by A32, XBOOLE_0:def 5;
f . i in fj by A29, A30, A34;
then x in union fj by A35, TARSKI:def 4;
hence contradiction by A31, A33, XBOOLE_0:def 5; :: thesis: verum

end;

thus for i, j being Nat st i <> j holds
g . i misses g . j :: thesis: for n being Nat ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) )

proof

let i, j be Nat; :: thesis: ( i <> j implies g . i misses g . j )
assume i <> j ; :: thesis: g . i misses g . j
then ( i < j or j < i ) by XXREAL_0:1;
hence g . i misses g . j by A28; :: thesis: verum

end;

let n be Nat; :: thesis: ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) )
n in NAT by ORDINAL1:def 12;
hence ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) by A10; :: thesis: verum