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 b2 being Real st b <= b2 & b2 < c holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,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 b2 being Real st b <= b2 & b2 < c holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,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 b2 being Real st b <= b2 & b2 < c holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c))
let b2 be Real; :: thesis: ( b <= b2 & b2 < c implies (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) )
assume A7: ( b <= b2 & b2 < c ) ; :: thesis: (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,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;
( ].a,b2.] c= ].a,c.[ & [.b,b2.] c= ].a,c.[ ) by A7, A2, XXREAL_1:47, XXREAL_1:49;
then A9: ( ].a,b2.] c= dom f & [.b,b2.] c= dom f ) by A1;
A10: ( f is_integrable_on ['b,b2'] & f | ['b,b2'] is bounded ) by A7, A4;

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 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,b2)) + (right_improper_integral (f,b2,c))

then A11: right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A4, Th39;
then A12: ( f is_right_improper_integrable_on b2,c & right_improper_integral (f,b2,c) = ext_right_integral (f,b2,c) ) by A7, A8, A4, Lm16;
A13: right_improper_integral (f,b,c) = (right_improper_integral (f,b2,c)) + (integral (f,b,b2)) by A7, A8, A10, A12, Lm20
.= (ext_right_integral (f,b2,c)) + (integral (f,b,b2)) by A12, XXREAL_3:def 2 ;

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 A14: 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,b2)) + (right_improper_integral (f,b2,c))

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

end;

suppose A16: 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,b2)) + (right_improper_integral (f,b2,c))

left_improper_integral (f,a,b2) = +infty by A7, A2, A9, A10, A3, A16, Lm13;
then (right_improper_integral (f,b2,c)) + (left_improper_integral (f,a,b2)) = +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,b2)) + (right_improper_integral (f,b2,c)) by A16, A11, XXREAL_3:def 2; :: thesis: verum

end;

suppose A17: 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,b2)) + (right_improper_integral (f,b2,c))

left_improper_integral (f,a,b2) = -infty by A7, A2, A9, A10, A3, A17, Lm14;
then (right_improper_integral (f,b2,c)) + (left_improper_integral (f,a,b2)) = -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,b2)) + (right_improper_integral (f,b2,c)) by A17, A11, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A18: 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,b2)) + (right_improper_integral (f,b2,c))

A19: right_improper_integral (f,b2,c) = +infty by A8, A4, A18, A7, Lm17;

per cases ( f is_left_ext_Riemann_integrable_on a,b or not f is_left_ext_Riemann_integrable_on a,b ) ;

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,b2)) + (right_improper_integral (f,b2,c))

then A20: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A3, Th34;
then left_improper_integral (f,a,b2) = (left_improper_integral (f,a,b)) + (integral (f,b,b2)) by A7, A2, A9, A10, A3, Lm12
.= (ext_left_integral (f,a,b)) + (integral (f,b,b2)) by A20, XXREAL_3:def 2 ;
then (right_improper_integral (f,b2,c)) + (left_improper_integral (f,a,b2)) = +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,b2)) + (right_improper_integral (f,b2,c)) by A18, A20, XXREAL_3:def 2; :: thesis: verum

end;

suppose not 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,b2)) + (right_improper_integral (f,b2,c))

then left_improper_integral (f,a,b) = +infty by A18, A5, A3, Th34;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) by A18, A19, A7, A2, A9, A10, A3, Lm13; :: thesis: verum

end;

end;

end;

suppose A21: 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,b2)) + (right_improper_integral (f,b2,c))

A22: right_improper_integral (f,b2,c) = -infty by A8, A4, A21, A7, Lm18;

per cases ( f is_left_ext_Riemann_integrable_on a,b or not f is_left_ext_Riemann_integrable_on a,b ) ;

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,b2)) + (right_improper_integral (f,b2,c))

then A23: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A3, Th34;
then left_improper_integral (f,a,b2) = (left_improper_integral (f,a,b)) + (integral (f,b,b2)) by A7, A2, A9, A10, A3, Lm12
.= (ext_left_integral (f,a,b)) + (integral (f,b,b2)) by A23, XXREAL_3:def 2 ;
then (right_improper_integral (f,b2,c)) + (left_improper_integral (f,a,b2)) = -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,b2)) + (right_improper_integral (f,b2,c)) by A21, A23, XXREAL_3:def 2; :: thesis: verum

end;

suppose not 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,b2)) + (right_improper_integral (f,b2,c))

then left_improper_integral (f,a,b) = -infty by A21, A6, A3, Th34;
hence (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b2)) + (right_improper_integral (f,b2,c)) by A21, A22, A7, A2, A9, A10, A3, Lm14; :: thesis: verum

end;

end;

end;

end;