let f be PartFunc of REAL,REAL; :: thesis: ( f is_integrable_on B-Meas implies ( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) ) )
assume f is_integrable_on B-Meas ; :: thesis: ( f is_integrable_on L-Meas & Integral (B-Meas,f) = Integral (L-Meas,f) )
then A1: R_EAL f is_integrable_on B-Meas by MESFUNC6:def 4;
hence f is_integrable_on L-Meas by Th38, MEASUR12:def 11, MEASUR12:def 12, MESFUNC6:def 4; :: thesis: Integral (B-Meas,f) = Integral (L-Meas,f)
( Integral (B-Meas,f) = Integral (B-Meas,(R_EAL f)) & Integral (L-Meas,f) = Integral (L-Meas,(R_EAL f)) ) by MESFUNC6:def 3;
hence Integral (B-Meas,f) = Integral (L-Meas,f) by A1, Th38, MEASUR12:def 11, MEASUR12:def 12; :: thesis: verum