theorem Th13: :: MESFUNC3:13

for X being non empty set
for S being SigmaField of X
for F being Finite_Sep_Sequence of S ex G being Finite_Sep_Sequence of S st
( union (rng F) = union (rng G) & ( for n being Nat st n in dom G holds
( G . n <> {} & ex m being Nat st
( m in dom F & F . m = G . n ) ) ) )