for X being non empty set
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 = {} ) )