let f be PartFunc of REAL,REAL; :: thesis: for b being Real st dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) holds
for b2 being Real st b <= b2 holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
let b be Real; :: thesis: ( dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) implies for b2 being Real st b <= b2 holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) )
assume that
A1: dom f = REAL and
A2: f is_-infty_improper_integrable_on b and
A3: f is_+infty_improper_integrable_on b and
A4: ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) and
A5: ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) ; :: thesis: for b2 being Real st b <= b2 holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
let b2 be Real; :: thesis: ( b <= b2 implies (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) )
assume A6: b <= b2 ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
A7: ( left_closed_halfline b c= dom f & right_closed_halfline b c= dom f ) by A1;
A8: ( left_closed_halfline b2 c= dom f & [.b,b2.] c= dom f ) by A1;
A9: ( f is_integrable_on ['b,b2'] & f | ['b,b2'] is bounded ) by A6, A3;

per cases ( f is_+infty_ext_Riemann_integrable_on b or improper_integral_+infty (f,b) = +infty or improper_integral_+infty (f,b) = -infty ) by A3, Th27;

suppose f is_+infty_ext_Riemann_integrable_on b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

then A10: improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A3, Th27;
then A11: ( f is_+infty_improper_integrable_on b2 & improper_integral_+infty (f,b2) = infty_ext_right_integral (f,b2) ) by A6, A1, A3, Th30;
A12: improper_integral_+infty (f,b) = (improper_integral_+infty (f,b2)) + (integral (f,b,b2)) by A6, A7, A9, A11, Th31
.= (infty_ext_right_integral (f,b2)) + (integral (f,b,b2)) by A11, XXREAL_3:def 2 ;

per cases ( f is_-infty_ext_Riemann_integrable_on b or improper_integral_-infty (f,b) = +infty or improper_integral_-infty (f,b) = -infty ) by A2, Th22;

suppose A13: f is_-infty_ext_Riemann_integrable_on b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

then A14: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A2, Th22;
then improper_integral_-infty (f,b2) = (improper_integral_-infty (f,b)) + (integral (f,b,b2)) by A6, A8, A9, A2, Lm7
.= (infty_ext_left_integral (f,b)) + (integral (f,b,b2)) by A14, XXREAL_3:def 2 ;
then (improper_integral_+infty (f,b2)) + (improper_integral_-infty (f,b2)) = (infty_ext_right_integral (f,b2)) + ((infty_ext_left_integral (f,b)) + (integral (f,b,b2))) by A11, XXREAL_3:def 2
.= ((infty_ext_right_integral (f,b2)) + (integral (f,b,b2))) + (infty_ext_left_integral (f,b))
.= (improper_integral_+infty (f,b)) + (infty_ext_left_integral (f,b)) by A12, XXREAL_3:def 2 ;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) by A13, A2, Th22; :: thesis: verum

end;

suppose A15: improper_integral_-infty (f,b) = +infty ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

improper_integral_-infty (f,b2) = +infty by A6, A8, A9, A2, A15, Lm8;
then (improper_integral_+infty (f,b2)) + (improper_integral_-infty (f,b2)) = +infty by A11, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) by A15, A10, XXREAL_3:def 2; :: thesis: verum

end;

suppose A16: improper_integral_-infty (f,b) = -infty ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

improper_integral_-infty (f,b2) = -infty by A6, A8, A9, A2, A16, Lm9;
then (improper_integral_+infty (f,b2)) + (improper_integral_-infty (f,b2)) = -infty by A11, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) by A16, A10, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A17: improper_integral_+infty (f,b) = +infty ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

A18: improper_integral_+infty (f,b2) = +infty by A1, A3, A17, A6, Th30;

per cases ( f is_-infty_ext_Riemann_integrable_on b or not f is_-infty_ext_Riemann_integrable_on b ) ;

suppose f is_-infty_ext_Riemann_integrable_on b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

then A19: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A2, Th22;
then improper_integral_-infty (f,b2) = (improper_integral_-infty (f,b)) + (integral (f,b,b2)) by A6, A8, A9, A2, Lm7
.= (infty_ext_left_integral (f,b)) + (integral (f,b,b2)) by A19, XXREAL_3:def 2 ;
then (improper_integral_+infty (f,b2)) + (improper_integral_-infty (f,b2)) = +infty by A18, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) by A17, A19, XXREAL_3:def 2; :: thesis: verum

end;

suppose not f is_-infty_ext_Riemann_integrable_on b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

then improper_integral_-infty (f,b) = +infty by A17, A4, A2, Th22;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) by A17, A18, A6, A8, A9, A2, Lm8; :: thesis: verum

end;

end;

end;

suppose A20: improper_integral_+infty (f,b) = -infty ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

A21: improper_integral_+infty (f,b2) = -infty by A1, A3, A20, A6, Th30;

per cases ( f is_-infty_ext_Riemann_integrable_on b or not f is_-infty_ext_Riemann_integrable_on b ) ;

suppose f is_-infty_ext_Riemann_integrable_on b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

then A22: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A2, Th22;
then improper_integral_-infty (f,b2) = (improper_integral_-infty (f,b)) + (integral (f,b,b2)) by A6, A8, A9, A2, Lm7
.= (infty_ext_left_integral (f,b)) + (integral (f,b,b2)) by A22, XXREAL_3:def 2 ;
then (improper_integral_+infty (f,b2)) + (improper_integral_-infty (f,b2)) = -infty by A21, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) by A20, A22, XXREAL_3:def 2; :: thesis: verum

end;

suppose not f is_-infty_ext_Riemann_integrable_on b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))

then improper_integral_-infty (f,b) = -infty by A20, A5, A2, Th22;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) by A20, A21, A6, A8, A9, A2, Lm9; :: thesis: verum

end;

end;

end;

end;