theorem Th55: :: MEASURE9:55

for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S ex 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)