let f be PartFunc of REAL,REAL; :: thesis: for a, b, c being Real st ].a,c.[ c= dom f & a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) holds
for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
let a, b, c be Real; :: thesis: ( ].a,c.[ c= dom f & a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) implies for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) )
assume that
A1: ].a,c.[ c= dom f and
A2: ( a < b & b < c ) and
A3: f is_left_improper_integrable_on a,b and
A4: f is_right_improper_integrable_on b,c and
A5: ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) and
A6: ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) ; :: thesis: for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
let b1 be Real; :: thesis: ( a < b1 & b1 <= b implies (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) )
assume A7: ( a < b1 & b1 <= b ) ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
( ].a,b.] c= ].a,c.[ & [.b,c.[ c= ].a,c.[ ) by A2, XXREAL_1:48, XXREAL_1:49;
then A8: ( ].a,b.] c= dom f & [.b,c.[ c= dom f ) by A1;
( [.b1,c.[ c= ].a,c.[ & [.b1,b.] c= ].a,c.[ ) by A7, A2, XXREAL_1:47, XXREAL_1:48;
then A9: ( [.b1,c.[ c= dom f & [.b1,b.] c= dom f ) by A1;
A10: ( f is_integrable_on ['b1,b'] & f | ['b1,b'] is bounded ) by A7, A3;

per cases ( f is_left_ext_Riemann_integrable_on a,b or left_improper_integral (f,a,b) = +infty or left_improper_integral (f,a,b) = -infty ) by A3, Th34;

suppose f is_left_ext_Riemann_integrable_on a,b ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

then A11: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A3, Th34;
then A12: ( f is_left_improper_integrable_on a,b1 & left_improper_integral (f,a,b1) = ext_left_integral (f,a,b1) ) by A7, A8, A3, Lm8;
A13: left_improper_integral (f,a,b) = (left_improper_integral (f,a,b1)) + (integral (f,b1,b)) by A7, A8, A10, A12, Lm12
.= (ext_left_integral (f,a,b1)) + (integral (f,b1,b)) by A12, XXREAL_3:def 2 ;

per cases ( f is_right_ext_Riemann_integrable_on b,c or right_improper_integral (f,b,c) = +infty or right_improper_integral (f,b,c) = -infty ) by A4, Th39;

suppose A14: f is_right_ext_Riemann_integrable_on b,c ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

then A15: right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A4, Th39;
then right_improper_integral (f,b1,c) = (right_improper_integral (f,b,c)) + (integral (f,b1,b)) by A7, A2, A9, A10, A4, Lm20
.= (ext_right_integral (f,b,c)) + (integral (f,b1,b)) by A15, XXREAL_3:def 2 ;
then (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = (ext_left_integral (f,a,b1)) + ((ext_right_integral (f,b,c)) + (integral (f,b1,b))) by A12, XXREAL_3:def 2
.= ((ext_left_integral (f,a,b1)) + (integral (f,b1,b))) + (ext_right_integral (f,b,c))
.= (left_improper_integral (f,a,b)) + (ext_right_integral (f,b,c)) by A13, XXREAL_3:def 2 ;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) by A14, A4, Th39; :: thesis: verum

end;

suppose A16: right_improper_integral (f,b,c) = +infty ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

right_improper_integral (f,b1,c) = +infty by A7, A2, A9, A10, A4, A16, Lm21;
then (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = +infty by A12, XXREAL_3:def 2;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) by A16, A11, XXREAL_3:def 2; :: thesis: verum

end;

suppose A17: right_improper_integral (f,b,c) = -infty ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

right_improper_integral (f,b1,c) = -infty by A7, A2, A9, A10, A4, A17, Lm22;
then (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = -infty by A12, XXREAL_3:def 2;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) by A17, A11, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A18: left_improper_integral (f,a,b) = +infty ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

A19: left_improper_integral (f,a,b1) = +infty by A8, A3, A18, A7, Lm9;

per cases ( f is_right_ext_Riemann_integrable_on b,c or not f is_right_ext_Riemann_integrable_on b,c ) ;

suppose f is_right_ext_Riemann_integrable_on b,c ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

then A20: right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A4, Th39;
then right_improper_integral (f,b1,c) = (right_improper_integral (f,b,c)) + (integral (f,b1,b)) by A7, A2, A9, A10, A4, Lm20
.= (ext_right_integral (f,b,c)) + (integral (f,b1,b)) by A20, XXREAL_3:def 2 ;
then (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = +infty by A19, XXREAL_3:def 2;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) by A18, A20, XXREAL_3:def 2; :: thesis: verum

end;

suppose not f is_right_ext_Riemann_integrable_on b,c ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

then right_improper_integral (f,b,c) = +infty by A18, A6, A4, Th39;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) by A18, A19, A7, A2, A9, A10, A4, Lm21; :: thesis: verum

end;

end;

end;

suppose A21: left_improper_integral (f,a,b) = -infty ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

A22: left_improper_integral (f,a,b1) = -infty by A8, A3, A21, A7, Lm10;

per cases ( f is_right_ext_Riemann_integrable_on b,c or not f is_right_ext_Riemann_integrable_on b,c ) ;

suppose f is_right_ext_Riemann_integrable_on b,c ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

then A23: right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A4, Th39;
then right_improper_integral (f,b1,c) = (right_improper_integral (f,b,c)) + (integral (f,b1,b)) by A7, A2, A9, A10, A4, Lm20
.= (ext_right_integral (f,b,c)) + (integral (f,b1,b)) by A23, XXREAL_3:def 2 ;
then (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = -infty by A22, XXREAL_3:def 2;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) by A21, A23, XXREAL_3:def 2; :: thesis: verum

end;

suppose not f is_right_ext_Riemann_integrable_on b,c ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))

then right_improper_integral (f,b,c) = -infty by A21, A5, A4, Th39;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) by A21, A22, A7, A2, A9, A10, A4, Lm22; :: thesis: verum

end;

end;

end;

end;