theorem Th11: :: MESFUN12:11

for X being non empty set
for S being SigmaField of X
for f being Function of X,ExtREAL
for E being Finite_Sep_Sequence of S
for F being summable FinSequence of Funcs (X,ExtREAL) st dom E = dom F & dom f = union (rng E) & ( for n being Nat st n in dom F holds
ex r being Real st F /. n = r (#) (chi ((E . n),X)) ) & f = (Partial_Sums F) /. (len F) holds
( ( for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & m <> n holds
(F /. n) . x = 0 ) & ( for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & n < m holds
((Partial_Sums F) /. n) . x = 0 ) & ( for x being Element of X
for m, n being Nat st m in dom F & n in dom F & x in E . m & n >= m holds
((Partial_Sums F) /. n) . x = f . x ) & ( for x being Element of X
for m being Nat st m in dom F & x in E . m holds
(F /. m) . x = f . x ) & f is_simple_func_in S )