theorem :: MEASURE8:31

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for SSets being SetSequence of S st SSets is non-ascending & M . (SSets . 0) < +infty holds
lim (M * SSets) = M . (lim SSets)