theorem :: MEASURE9:52

for X being set
for P being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for K being disjoint_valued Function of NAT,(Ring_generated_by P) st rng K is with_non-empty_element holds
ex Y being non empty FinSequenceSet of P st
( Y = { F where F is disjoint_valued FinSequence of P : ( Union F in rng K & F <> {} ) } & Y is with_non-empty_elements )