theorem :: MESFUNC6:75

for X being non empty set
for S being SigmaField of X
for A being Element of S
for r being Real ex f being PartFunc of X,REAL st
( f is_simple_func_in S & dom f = A & ( for x being object st x in A holds
f . x = r ) )