let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real
for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b & f | A is nonnegative holds
( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
let a, b be Real; :: thesis: for A being non empty Subset of REAL st ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b & f | A is nonnegative holds
( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
let A be non empty Subset of REAL; :: thesis: ( ].a,b.] c= dom f & A = ].a,b.] & f is_left_improper_integrable_on a,b & abs f is_left_ext_Riemann_integrable_on a,b & f | A is nonnegative implies ( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) ) )
assume that
A1: ].a,b.] c= dom f and
A2: A = ].a,b.] and
A3: f is_left_improper_integrable_on a,b and
A4: abs f is_left_ext_Riemann_integrable_on a,b and
A5: f | A is nonnegative ; :: thesis: ( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
a < b by A2, XXREAL_1:26;
then f is_left_ext_Riemann_integrable_on a,b by A1, A3, A4, Th58;
hence ( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) ) by A1, A2, A3, A5, Th43; :: thesis: verum