theorem Th49: :: MESFUNC6:49

for X being non empty set
for S being SigmaField of X
for f being PartFunc of X,REAL holds
( f is_simple_func_in S iff R_EAL f is_simple_func_in S ) by MESFUNC2:def 4;