theorem Th49: :: MESFUN14:49

for A being non empty closed_interval Subset of REAL
for A1 being Element of L-Field
for f being PartFunc of REAL,REAL st A = A1 & A c= dom f & f || A is bounded & f is_integrable_on A holds
( f is A1 -measurable & f | A1 is_integrable_on L-Meas & integral (f || A) = Integral (L-Meas,(f | A)) )