theorem Th33: :: TOPDIM_1:33

for X being set
for f being SetSequence of X ex g being SetSequence of X st
( union (rng f) = union (rng g) & ( for i, j being Nat st i <> j holds
g . i misses g . j ) & ( for n being Nat ex fn being finite Subset-Family of X st
( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) ) )