for f being PartFunc of REAL,ExtREAL st f is_integrable_on B-Meas holds
( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) ) by Th38, MEASUR12:def 11, MEASUR12:def 12;