theorem Th46: :: MEASURE9:48

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 zeroed nonnegative additive Function of (Ring_generated_by S),ExtREAL st
for A being set st A in Ring_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F)