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_improper_integrable_on a,b & ex c being Real st
( a < c & c < b & abs f is_left_ext_Riemann_integrable_on a,c & abs f is_right_ext_Riemann_integrable_on c,b ) holds
( f | A is_integrable_on L-Meas & 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_improper_integrable_on a,b & ex c being Real st
( a < c & c < b & abs f is_left_ext_Riemann_integrable_on a,c & abs f is_right_ext_Riemann_integrable_on c,b ) holds
( f | A is_integrable_on L-Meas & 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_improper_integrable_on a,b & ex c being Real st
( a < c & c < b & abs f is_left_ext_Riemann_integrable_on a,c & abs f is_right_ext_Riemann_integrable_on c,b ) implies ( f | A is_integrable_on L-Meas & 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_improper_integrable_on a,b
and
A4:
ex c being Real st
( a < c & c < b & abs f is_left_ext_Riemann_integrable_on a,c & abs f is_right_ext_Riemann_integrable_on c,b )
; ( f | A is_integrable_on L-Meas & improper_integral (f,a,b) = Integral (L-Meas,(f | A)) )
consider c being Real such that
A5:
( a < c & c < b )
and
A6:
abs f is_left_ext_Riemann_integrable_on a,c
and
A7:
abs f is_right_ext_Riemann_integrable_on c,b
by A4;
reconsider AC = ].a,c.] as non empty Subset of REAL by A5, XXREAL_1:32;
reconsider CB = [.c,b.[ as non empty Subset of REAL by A5, XXREAL_1:31;
reconsider AC = AC, CB = CB as Element of L-Field by MEASUR10:5, MEASUR12:75;
A8:
( f is_left_improper_integrable_on a,c & f is_right_improper_integrable_on c,b & improper_integral (f,a,b) = (left_improper_integral (f,a,c)) + (right_improper_integral (f,c,b)) )
by A1, A3, A5, INTEGR24:48;
A9:
AC \/ CB = A
by A2, A5, XXREAL_1:172;
A10:
( AC c= ].a,b.[ & CB c= ].a,b.[ )
by A5, XXREAL_1:48, XXREAL_1:49;
then A11:
( AC c= dom f & CB c= dom f )
by A1;
then A12:
( f | AC is_integrable_on L-Meas & left_improper_integral (f,a,c) = Integral (L-Meas,(f | AC)) )
by A6, A8, Th81;
( f | CB is_integrable_on L-Meas & right_improper_integral (f,c,b) = Integral (L-Meas,(f | CB)) )
by A7, A8, A11, Th80;
then A13:
f | (AC \/ CB) is_integrable_on L-Meas
by A11, A12, Th53;
hence
f | A is_integrable_on L-Meas
by A2, A5, XXREAL_1:172; improper_integral (f,a,b) = Integral (L-Meas,(f | A))
set C = {c};
A14:
{c} = [.c,c.]
by XXREAL_1:17;
reconsider C = {c} as Element of L-Field by Th28;
A15: L-Meas . C =
c - c
by A14, MESFUN14:5
.=
0
;
A16:
dom (f | AC) = AC
by A11, RELAT_1:62;
then A17:
dom (R_EAL (f | AC)) = AC
by MESFUNC5:def 7;
R_EAL (f | AC) is_integrable_on L-Meas
by A11, A6, A8, Th81, MESFUNC6:def 4;
then consider E being Element of L-Field such that
A18:
( E = dom (R_EAL (f | AC)) & R_EAL (f | AC) is E -measurable )
by MESFUNC5:def 17;
A19:
AC \ C = ].a,c.[
by A5, XXREAL_1:137;
AC \ C c= AC
by XBOOLE_1:36;
then
AC \ C c= A
by A10, A2;
then A20:
( (f | A) | (AC \ C) = f | (AC \ C) & (f | AC) | (AC \ C) = f | (AC \ C) & (f | A) | CB = f | CB )
by A2, A5, XXREAL_1:48, XBOOLE_1:36, RELAT_1:74;
Integral (L-Meas,((f | A) | A)) =
Integral (L-Meas,((f | A) | ((AC \ C) \/ CB)))
by A2, A5, A19, XXREAL_1:173
.=
(Integral (L-Meas,((f | A) | (AC \ C)))) + (Integral (L-Meas,((f | A) | CB)))
by A13, A9, A19, XXREAL_1:94, MESFUNC6:92
.=
(Integral (L-Meas,(f | AC))) + (Integral (L-Meas,(f | CB)))
by A20, A18, A16, A15, A17, MESFUNC6:def 1, MESFUNC6:89
;
hence
improper_integral (f,a,b) = Integral (L-Meas,(f | A))
by A8, A12, A7, A11, Th80; verum