theorem Th5: :: MESFUN12:5

for X being non empty set
for S being SigmaField of X
for f being non empty PartFunc of X,ExtREAL
for M being sigma_Measure of S st f is_simple_func_in S holds
ex E being non empty Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL ex r being FinSequence of REAL st
( E,a are_Re-presentation_of f & ( for n being Nat holds
( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),X)) | (E . n) & ( E . n = {} implies r . n = 0 ) ) ) )