theorem Th46: :: MESFUN14:46

for f being PartFunc of REAL,REAL
for a being Real st a in dom f holds
ex A being Element of Borel_Sets st
( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )