theorem Th24: :: MEASURE8:24

for X being set
for C being C_Measure of X
for seq being Sep_Sequence of (sigma_Field C) holds
( union (rng seq) in sigma_Field C & C . (union (rng seq)) = Sum (C * seq) )