theorem :: MEASURE2:23

for X being set
for S being SigmaField of X
for M being sigma_Measure of S
for F being sequence of S st ( for n being Nat holds F . n c= F . (n + 1) ) holds
M . (union (rng F)) = sup (rng (M * F))