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 S_{1}[ 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 & S_{1}[x1,y1] )

A7: for x1 being object st x1 in NAT holds

S_{1}[x1,G . x1]
from FUNCT_2:sch 1(A2);

for n, m being object st n <> m holds

G . n misses G . m

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)

for x1 being object st x1 in union (rng G) holds

x1 in 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 = {} ) )

m in NAT by ORDINAL1:def 12;

hence ( not m in dom F implies G . m = {} ) by A7; :: thesis: verum

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 S

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 & S

proof

consider G being sequence of S such that
let x1 be object ; :: thesis: ( x1 in NAT implies ex y1 being object st

( y1 in S & S_{1}[x1,y1] ) )

assume x1 in NAT ; :: thesis: ex y1 being object st

( y1 in S & S_{1}[x1,y1] )

then reconsider x1 = x1 as Element of NAT ;

end;( y1 in S & S

assume x1 in NAT ; :: thesis: ex y1 being object st

( y1 in S & S

then reconsider x1 = x1 as Element of NAT ;

per cases
( x1 in dom F or not x1 in dom F )
;

end;

suppose A3:
x1 in dom F
; :: thesis: ex y1 being object st

( y1 in S & S_{1}[x1,y1] )

( y1 in S & S

then A4:
F . x1 in rng F
by FUNCT_1:def 3;

A5: rng F c= S by A1, FINSEQ_1:def 4;

take F . x1 ; :: thesis: ( F . x1 in S & S_{1}[x1,F . x1] )

thus ( F . x1 in S & S_{1}[x1,F . x1] )
by A3, A4, A5; :: thesis: verum

end;A5: rng F c= S by A1, FINSEQ_1:def 4;

take F . x1 ; :: thesis: ( F . x1 in S & S

thus ( F . x1 in S & S

suppose A6:
not x1 in dom F
; :: thesis: ex y1 being object st

( y1 in S & S_{1}[x1,y1] )

( y1 in S & S

take
{}
; :: thesis: ( {} in S & S_{1}[x1, {} ] )

thus ( {} in S & S_{1}[x1, {} ] )
by A6, PROB_1:4; :: thesis: verum

end;thus ( {} in S & S

A7: for x1 being object st x1 in NAT holds

S

for n, m being object st n <> m holds

G . n misses G . m

proof

then reconsider G = G as Sep_Sequence of S by PROB_2:def 2;
let n, m be object ; :: thesis: ( n <> m implies G . n misses G . m )

assume A8: n <> m ; :: thesis: G . n misses G . m

end;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 )
;

end;

suppose A9:
( n in NAT & m in NAT )
; :: thesis: G . n misses G . m

end;

now :: thesis: G . n misses G . mend;

hence
G . n misses G . m
; :: thesis: verumper cases
( ( n in dom F & m in dom F ) or not n in dom F or not m in dom F )
;

end;

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 A1, A8, PROB_2:def 2; :: thesis: verum

end;hence G . n misses G . m by A1, A8, PROB_2:def 2; :: thesis: verum

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

then A16:
union (rng F) c= union (rng G)
;
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 A12, FUNCT_1:def 3;

dom F c= NAT by A1, RELAT_1:def 18;

then reconsider k = k as Element of NAT by A13;

A15: F . k = G . k by A7, A13;

G . k in rng G by FUNCT_2:4;

hence x1 in union (rng G) by A11, A14, A15, TARSKI:def 4; :: thesis: verum

end;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 A12, FUNCT_1:def 3;

dom F c= NAT by A1, RELAT_1:def 18;

then reconsider k = k as Element of NAT by A13;

A15: F . k = G . k by A7, A13;

G . k in rng G by FUNCT_2:4;

hence x1 in union (rng G) by A11, A14, A15, TARSKI:def 4; :: thesis: verum

for x1 being object st x1 in union (rng G) holds

x1 in union (rng F)

proof

then
union (rng G) c= union (rng F)
;
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 A18, FUNCT_1:def 3;

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 A21, FUNCT_1:def 3;

hence x1 in union (rng F) by A17, A20, A22, TARSKI:def 4; :: thesis: verum

end;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 A18, FUNCT_1:def 3;

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 A21, FUNCT_1:def 3;

hence x1 in union (rng F) by A17, A20, A22, TARSKI:def 4; :: thesis: verum

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 m be Nat; :: thesis: ( not m in dom F implies G . m = {} )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;n in NAT by ORDINAL1:def 12;

hence ( n in dom F implies F . n = G . n ) by A7; :: thesis: verum

m in NAT by ORDINAL1:def 12;

hence ( not m in dom F implies G . m = {} ) by A7; :: thesis: verum