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

union (rng F) in S

let S be SigmaField of X; :: thesis: for F being Function st F is Finite_Sep_Sequence of S holds

union (rng F) in S

let F be Function; :: thesis: ( F is Finite_Sep_Sequence of S implies union (rng F) in S )

assume F is Finite_Sep_Sequence of S ; :: thesis: union (rng F) in S

then 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 = {} ) ) by Th30;

hence union (rng F) in S ; :: thesis: verum

for F being Function st F is Finite_Sep_Sequence of S holds

union (rng F) in S

let S be SigmaField of X; :: thesis: for F being Function st F is Finite_Sep_Sequence of S holds

union (rng F) in S

let F be Function; :: thesis: ( F is Finite_Sep_Sequence of S implies union (rng F) in S )

assume F is Finite_Sep_Sequence of S ; :: thesis: union (rng F) in S

then 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 = {} ) ) by Th30;

hence union (rng F) in S ; :: thesis: verum