theorem :: MEASURE9:51

for X, Z 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 Z = { [n,F] where n is Nat, F is disjoint_valued FinSequence of P : ( Union F = K . n & ( K . n = {} implies F = <*{}*> ) ) } holds
( proj2 Z is FinSequenceSet of P & ( for x being object holds
( x in rng K iff ex F being FinSequence of P st
( F in proj2 Z & Union F = x ) ) ) & proj2 Z is with_non-empty_elements )