for X being set
for F being Field_Subset of X
for M being Measure of F
for k being Nat
for FSets being Set_Sequence of F st ( for n being Nat holds M . (FSets . n) < +infty ) holds
M . ((Partial_Union FSets) . k) < +infty