theorem Th58: :: MEASURE9:58

for X being set
for S being Field_Subset of X
for M being Measure of S
for F being Sep_Sequence of S
for n being Nat holds
( union (rng (F | (Segm (n + 1)))) in S & (Partial_Sums (M * F)) . n = M . (union (rng (F | (Segm (n + 1))))) )