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