let X be non empty set ; :: thesis: for S being SigmaField of X
for F being Function st F is Finite_Sep_Sequence of S holds
ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )

let S be SigmaField of X; :: thesis: for F being Function st F is Finite_Sep_Sequence of S holds
ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )

let F be Function; :: thesis: ( F is Finite_Sep_Sequence of S implies ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) ) )

defpred S1[ object , object ] means ( ( \$1 in dom F implies F . \$1 = \$2 ) & ( not \$1 in dom F implies \$2 = {} ) );
assume A1: F is Finite_Sep_Sequence of S ; :: thesis: ex G being Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )

A2: for x1 being object st x1 in NAT holds
ex y1 being object st
( y1 in S & S1[x1,y1] )
proof
let x1 be object ; :: thesis: ( x1 in NAT implies ex y1 being object st
( y1 in S & S1[x1,y1] ) )

assume x1 in NAT ; :: thesis: ex y1 being object st
( y1 in S & S1[x1,y1] )

then reconsider x1 = x1 as Element of NAT ;
per cases ( x1 in dom F or not x1 in dom F ) ;
suppose A3: x1 in dom F ; :: thesis: ex y1 being object st
( y1 in S & S1[x1,y1] )

then A4: F . x1 in rng F by FUNCT_1:def 3;
A5: rng F c= S by ;
take F . x1 ; :: thesis: ( F . x1 in S & S1[x1,F . x1] )
thus ( F . x1 in S & S1[x1,F . x1] ) by A3, A4, A5; :: thesis: verum
end;
suppose A6: not x1 in dom F ; :: thesis: ex y1 being object st
( y1 in S & S1[x1,y1] )

take {} ; :: thesis: ( {} in S & S1[x1, {} ] )
thus ( {} in S & S1[x1, {} ] ) by ; :: thesis: verum
end;
end;
end;
consider G being sequence of S such that
A7: for x1 being object st x1 in NAT holds
S1[x1,G . x1] from for n, m being object st n <> m holds
G . n misses G . m
proof
let n, m be object ; :: thesis: ( n <> m implies G . n misses G . m )
assume A8: n <> m ; :: thesis: G . n misses G . m
per cases ( ( n in NAT & m in NAT ) or not n in NAT or not m in NAT ) ;
suppose A9: ( n in NAT & m in NAT ) ; :: thesis: G . n misses G . m
now :: thesis: G . n misses G . m
per cases ( ( n in dom F & m in dom F ) or not n in dom F or not m in dom F ) ;
suppose ( n in dom F & m in dom F ) ; :: thesis: G . n misses G . m
then ( G . n = F . n & G . m = F . m ) by A7, A9;
hence G . n misses G . m by ; :: thesis: verum
end;
suppose A10: ( not n in dom F or not m in dom F ) ; :: thesis: G . n misses G . m
now :: thesis: G . n misses G . m
per cases ( not n in dom F or not m in dom F ) by A10;
suppose not n in dom F ; :: thesis: G . n misses G . m
then G . n = {} by A7, A9;
hence G . n misses G . m ; :: thesis: verum
end;
suppose not m in dom F ; :: thesis: G . n misses G . m
then G . m = {} by A7, A9;
hence G . n misses G . m ; :: thesis: verum
end;
end;
end;
hence G . n misses G . m ; :: thesis: verum
end;
end;
end;
hence G . n misses G . m ; :: thesis: verum
end;
suppose ( not n in NAT or not m in NAT ) ; :: thesis: G . n misses G . m
then ( not n in dom G or not m in dom G ) ;
then ( G . n = {} or G . m = {} ) by FUNCT_1:def 2;
hence G . n misses G . m ; :: thesis: verum
end;
end;
end;
then reconsider G = G as Sep_Sequence of S by PROB_2:def 2;
take G ; :: thesis: ( union (rng F) = union (rng G) & ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )

for x1 being object st x1 in union (rng F) holds
x1 in union (rng G)
proof
let x1 be object ; :: thesis: ( x1 in union (rng F) implies x1 in union (rng G) )
assume x1 in union (rng F) ; :: thesis: x1 in union (rng G)
then consider Y being set such that
A11: x1 in Y and
A12: Y in rng F by TARSKI:def 4;
consider k being object such that
A13: k in dom F and
A14: Y = F . k by ;
dom F c= NAT by ;
then reconsider k = k as Element of NAT by A13;
A15: F . k = G . k by ;
G . k in rng G by FUNCT_2:4;
hence x1 in union (rng G) by ; :: thesis: verum
end;
then A16: union (rng F) c= union (rng G) ;
for x1 being object st x1 in union (rng G) holds
x1 in union (rng F)
proof
let x1 be object ; :: thesis: ( x1 in union (rng G) implies x1 in union (rng F) )
assume x1 in union (rng G) ; :: thesis: x1 in union (rng F)
then consider Y being set such that
A17: x1 in Y and
A18: Y in rng G by TARSKI:def 4;
consider k being object such that
A19: k in dom G and
A20: Y = G . k by ;
reconsider k = k as Element of NAT by A19;
A21: k in dom F by A7, A17, A20;
A22: F . k = G . k by A7, A17, A20;
F . k in rng F by ;
hence x1 in union (rng F) by ; :: thesis: verum
end;
then union (rng G) c= union (rng F) ;
hence union (rng F) = union (rng G) by A16; :: thesis: ( ( for n being Nat st n in dom F holds
F . n = G . n ) & ( for m being Nat st not m in dom F holds
G . m = {} ) )

hereby :: thesis: for m being Nat st not m in dom F holds
G . m = {}
let n be Nat; :: thesis: ( n in dom F implies F . n = G . n )
n in NAT by ORDINAL1:def 12;
hence ( n in dom F implies F . n = G . n ) by A7; :: thesis: verum
end;
let m be Nat; :: thesis: ( not m in dom F implies G . m = {} )
m in NAT by ORDINAL1:def 12;
hence ( not m in dom F implies G . m = {} ) by A7; :: thesis: verum