let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let F be Function; :: thesis:
defpred S₁[ set , set ] 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:
A2: for x1 being set st x1 in NAT holds
ex y1 being set st
( y1 in S & S₁[x1,y1] )

proof

let x1 be set ; :: thesis:
assume A3: x1 in NAT ; :: thesis:
reconsider x1 = x1 as Element of NAT by A3;

per cases ;

suppose A4: x1 in dom F ; :: thesis:

A5: F . x1 in rng F by A4, FUNCT_1:def 5;
A6: rng F c= S by A1, FINSEQ_1:def 4;
take F . x1 ; :: thesis:
thus ( F . x1 in S & S₁[x1,F . x1] ) by A4, A5, A6; :: thesis:

end;

suppose A7: not x1 in dom F ; :: thesis:

take {} ; :: thesis:
thus ( {} in S & S₁[x1, {} ] ) by A7, PROB_1:10; :: thesis:

end;

end;

end;

consider G being Function of NAT ,S such that
A8: for x1 being set st x1 in NAT holds
S₁[x1,G . x1] from FUNCT_2:sch 1(A2);
A9: for n, m being set st n <> m holds
G . n misses G . m

proof

let n, m be set ; :: thesis:
assume A10: n <> m ; :: thesis:

per cases ;

suppose A11: ( n in NAT & m in NAT ) ; :: thesis:

A12: now

per cases ;

suppose A13: ( n in dom F & m in dom F ) ; :: thesis:

A14: ( G . n = F . n & G . m = F . m ) by A8, A11, A13;
thus G . n misses G . m by A1, A10, A14, PROB_2:def 3; :: thesis:

end;

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

A16: now

per cases by A15;

suppose A17: not n in dom F ; :: thesis:

A18: G . n = {} by A8, A11, A17;
thus G . n misses G . m by A18, XBOOLE_1:65; :: thesis:

end;

suppose A19: not m in dom F ; :: thesis:

A20: G . m = {} by A8, A11, A19;
thus G . n misses G . m by A20, XBOOLE_1:65; :: thesis:

end;

end;

end;

thus G . n misses G . m by A16; :: thesis:

end;

end;

end;

thus G . n misses G . m by A12; :: thesis:

end;

suppose A21: ( not n in NAT or not m in NAT ) ; :: thesis:

A22: ( not n in dom G or not m in dom G ) by A21;
A23: ( G . n = {} or G . m = {} ) by A22, FUNCT_1:def 4;
thus G . n misses G . m by A23, XBOOLE_1:65; :: thesis:

end;

end;

end;

reconsider G = G as Sep_Sequence of S by A9, PROB_2:def 3;
take G ; :: thesis:
A24: for x1 being set st x1 in union (rng F) holds
x1 in union (rng G)

proof

let x1 be set ; :: thesis:
assume A25: x1 in union (rng F) ; :: thesis:
consider Y being set such that
A26: x1 in Y and
A27: Y in rng F by A25, TARSKI:def 4;
consider k being set such that
A28: k in dom F and
A29: Y = F . k by A27, FUNCT_1:def 5;
A30: dom F c= NAT by A1, RELAT_1:def 18;
reconsider k = k as Element of NAT by A28, A30;
A31: F . k = G . k by A8, A28;
A32: G . k in rng G by FUNCT_2:6;
thus x1 in union (rng G) by A26, A29, A31, A32, TARSKI:def 4; :: thesis:

end;

A33: union (rng F) c= union (rng G) by A24, TARSKI:def 3;
A34: for x1 being set st x1 in union (rng G) holds
x1 in union (rng F)

proof

let x1 be set ; :: thesis:
assume A35: x1 in union (rng G) ; :: thesis:
consider Y being set such that
A36: x1 in Y and
A37: Y in rng G by A35, TARSKI:def 4;
consider k being set such that
A38: k in dom G and
A39: Y = G . k by A37, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A38;
A40: k in dom F by A8, A36, A39;
A41: F . k = G . k by A8, A36, A39;
A42: F . k in rng F by A40, FUNCT_1:def 5;
thus x1 in union (rng F) by A36, A39, A41, A42, TARSKI:def 4; :: thesis:

end;

A43: union (rng G) c= union (rng F) by A34, TARSKI:def 3;
thus union (rng F) = union (rng G) by A33, A43, XBOOLE_0:def 10; :: thesis:

hereby :: thesis:

let n be Nat; :: thesis:
A44: n in NAT by ORDINAL1:def 13;
thus ( n in dom F implies F . n = G . n ) by A8, A44; :: thesis:

end;

let m be Nat; :: thesis:
A45: m in NAT by ORDINAL1:def 13;
thus ( not m in dom F implies G . m = {} ) by A8, A45; :: thesis: