let f be PartFunc of REAL,REAL; 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 holds
( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
let a, b be 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 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; ( ].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 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
; ( f | A is_integrable_on L-Meas & left_improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
A5:
dom (max+ f) = dom f
by RFUNCT_3:def 10;
A6:
a < b
by A2, XXREAL_1:26;
then A7:
f is_left_ext_Riemann_integrable_on a,b
by A1, A3, A4, Th58;
then A8:
max+ f is_left_improper_integrable_on a,b
by A1, A4, A6, Th63, INTEGR24:32;
A9:
max+ f is_left_ext_Riemann_integrable_on a,b
by A1, A4, A2, A7, Th63, XXREAL_1:26;
then A10:
abs (max+ f) is_left_ext_Riemann_integrable_on a,b
by MESFUNC6:61, LPSPACE2:14;
A11:
(max+ f) | A is nonnegative
by MESFUNC6:61, MESFUNC6:55;
then
(max+ f) | A is_integrable_on L-Meas
by A1, A5, A2, A8, A10, Th75;
then A12:
max+ (f | A) is_integrable_on L-Meas
by MESFUNC6:66;
max+ (R_EAL (f | A)) = max+ (f | A)
by MESFUNC6:30;
then A13:
max+ (R_EAL (f | A)) = R_EAL (max+ (f | A))
by MESFUNC5:def 7;
then A14:
max+ (R_EAL (f | A)) is_integrable_on L-Meas
by A12, MESFUNC6:def 4;
A15:
dom (max- f) = dom f
by RFUNCT_3:def 11;
A16:
max- f is_left_improper_integrable_on a,b
by A1, A4, A6, A7, Th67, INTEGR24:32;
A17:
max- f is_left_ext_Riemann_integrable_on a,b
by A1, A4, A2, A7, Th67, XXREAL_1:26;
then A18:
abs (max- f) is_left_ext_Riemann_integrable_on a,b
by LPSPACE2:14, MESFUNC6:61;
A19:
(max- f) | A is nonnegative
by MESFUNC6:61, MESFUNC6:55;
then
(max- f) | A is_integrable_on L-Meas
by A1, A15, A2, A16, A18, Th75;
then A20:
max- (f | A) is_integrable_on L-Meas
by MESFUNC6:66;
max- (R_EAL (f | A)) = max- (f | A)
by MESFUNC6:30;
then A21:
max- (R_EAL (f | A)) = R_EAL (max- (f | A))
by MESFUNC5:def 7;
then
max- (R_EAL (f | A)) is_integrable_on L-Meas
by A20, MESFUNC6:def 4;
hence
f | A is_integrable_on L-Meas
by A14, MESFUN13:18, MESFUNC6:def 4; left_improper_integral (f,a,b) = Integral (L-Meas,(f | A))
reconsider A1 = A as Element of L-Field by A2, MEASUR12:72, MEASUR12:75;
R_EAL (f | A) is_integrable_on L-Meas
by A21, A14, A20, MESFUNC6:def 4, MESFUN13:18;
then consider E being Element of L-Field such that
A22:
( E = dom (R_EAL (f | A)) & R_EAL (f | A) is E -measurable )
by MESFUNC5:def 17;
A23:
left_improper_integral (f,a,b) = (left_improper_integral ((max+ f),a,b)) - (left_improper_integral ((max- f),a,b))
by A1, A9, A17, Th71;
A24: left_improper_integral ((max+ f),a,b) =
Integral (L-Meas,((max+ f) | A))
by A1, A5, A2, A8, A10, A11, Th75
.=
Integral (L-Meas,(max+ (f | A)))
by MESFUNC6:66
.=
Integral (L-Meas,(max+ (R_EAL (f | A))))
by A13, MESFUNC6:def 3
;
left_improper_integral ((max- f),a,b) =
Integral (L-Meas,((max- f) | A))
by A1, A15, A2, A16, A18, A19, Th75
.=
Integral (L-Meas,(max- (f | A)))
by MESFUNC6:66
.=
Integral (L-Meas,(max- (R_EAL (f | A))))
by A21, MESFUNC6:def 3
;
then
left_improper_integral (f,a,b) = Integral (L-Meas,(R_EAL (f | A)))
by A22, A23, A24, MESFUN11:54;
hence
left_improper_integral (f,a,b) = Integral (L-Meas,(f | A))
by MESFUNC6:def 3; verum