theorem :: MEASURE9:50

for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S ex M being Function of (Ring_generated_by S),ExtREAL st
( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K) ) )