theorem Th25: :: MEASUR10:26

for X being non empty set
for S being non empty Subset-Family of X
for f being Function of NAT,S
for F being Functional_Sequence of X,ExtREAL st f is disjoint_valued & ( for n being Nat holds F . n = chi ((f . n),X) ) holds
for x being object st x in X holds
(chi ((Union f),X)) . x = (lim (Partial_Sums F)) . x