theorem Th59: :: MEASURE9:59

for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being Measure of (Field_generated_by S) st ( for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F) ) holds
M is completely-additive