for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,COMPLEX st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) )