theorem Th9: :: MESFUNC3:9

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S holds M . (union (rng F)) = Sum (M * F)