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
union (rng F) in S