for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st
( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) )