let f be PartFunc of REAL,REAL; for a, c being Real st ].a,c.[ c= dom f & f is_improper_integrable_on a,c holds
for b being Real st a < b & b < c holds
( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )
let a, c be Real; ( ].a,c.[ c= dom f & f is_improper_integrable_on a,c implies for b being Real st a < b & b < c holds
( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) ) )
assume that
A1:
].a,c.[ c= dom f
and
A2:
f is_improper_integrable_on a,c
; for b being Real st a < b & b < c holds
( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )
let b be Real; ( a < b & b < c implies ( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) ) )
assume A3:
( a < b & b < c )
; ( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )
consider b1 being Real such that
A4:
( a < b1 & b1 < c )
and
A5:
f is_left_improper_integrable_on a,b1
and
A6:
f is_right_improper_integrable_on b1,c
and
A7:
improper_integral (f,a,c) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A1, A2, Def6;
per cases
( b < b1 or b >= b1 )
;
suppose A8:
b < b1
;
( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )
].a,b1.] c= ].a,c.[
by A4, XXREAL_1:49;
then A9:
].a,b1.] c= dom f
by A1;
[.b,c.[ c= ].a,c.[
by A3, XXREAL_1:48;
then A10:
[.b,c.[ c= dom f
by A1;
A11:
(
f | ['b,b1'] is
bounded &
f is_integrable_on ['b,b1'] )
by A5, A3, A8;
thus
f is_left_improper_integrable_on a,
b
by A3, A5, A8, A9, Th37;
( f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )thus
f is_right_improper_integrable_on b,
c
by A4, A8, A6, A10, A11, Th43;
improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c))thus
improper_integral (
f,
a,
c)
= (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c))
by A1, A2, A3, A4, A7, Th47;
verum end; suppose A12:
b >= b1
;
( f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )
].a,b.] c= ].a,c.[
by A3, XXREAL_1:49;
then A13:
].a,b.] c= dom f
by A1;
A14:
(
f | ['b1,b'] is
bounded &
f is_integrable_on ['b1,b'] )
by A6, A3, A12;
[.b1,c.[ c= ].a,c.[
by A4, XXREAL_1:48;
then A15:
[.b1,c.[ c= dom f
by A1;
thus
f is_left_improper_integrable_on a,
b
by A4, A5, A12, A13, A14, Th38;
( f is_right_improper_integrable_on b,c & improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) )thus
f is_right_improper_integrable_on b,
c
by A12, A3, A15, A6, Th42;
improper_integral (f,a,c) = (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c))thus
improper_integral (
f,
a,
c)
= (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c))
by A1, A2, A3, A4, A7, Th47;
verum end;