theorem Th42: :: MEASURE9:44

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
for A being set st A in Ring_generated_by S holds
for F1, F2 being disjoint_valued FinSequence of S st A = Union F1 & A = Union F2 holds
Sum (P * F1) = Sum (P * F2)