for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for r being Real st dom f in S & ( for x being object st x in dom f holds
f . x = r ) holds
f is_simple_func_in S