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 b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
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 b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) )
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 b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
A6: ( left_closed_halfline b c= dom f & right_closed_halfline b c= dom f ) by A1;
let b1 be Real; :: thesis: ( b1 <= b implies (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) )
assume A7: b1 <= b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
then A8: ( f is_integrable_on ['b1,b'] & f | ['b1,b'] is bounded ) by A2;
A9: ( right_closed_halfline b1 c= dom f & [.b1,b.] c= dom f ) by A1;

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 f is_-infty_ext_Riemann_integrable_on b ; :: thesis: (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))

then A10: improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) by A2, Th22;
then A11: ( f is_-infty_improper_integrable_on b1 & improper_integral_-infty (f,b1) = infty_ext_left_integral (f,b1) ) by A1, A7, A2, Lm3;
A12: improper_integral_-infty (f,b) = (improper_integral_-infty (f,b1)) + (integral (f,b1,b)) by A7, A6, A8, A11, Lm7
.= (infty_ext_left_integral (f,b1)) + (integral (f,b1,b)) 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 A3, Th27;

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,b1)) + (improper_integral_+infty (f,b1))

then A14: improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A3, Th27;
then improper_integral_+infty (f,b1) = (improper_integral_+infty (f,b)) + (integral (f,b1,b)) by A7, A9, A8, A3, Th31
.= (infty_ext_right_integral (f,b)) + (integral (f,b1,b)) by A14, XXREAL_3:def 2 ;
then (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (infty_ext_left_integral (f,b1)) + ((infty_ext_right_integral (f,b)) + (integral (f,b1,b))) by A11, XXREAL_3:def 2
.= ((infty_ext_left_integral (f,b1)) + (integral (f,b1,b))) + (infty_ext_right_integral (f,b))
.= (improper_integral_-infty (f,b)) + (infty_ext_right_integral (f,b)) by A12, XXREAL_3:def 2 ;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) by A13, A3, Th27; :: 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,b1)) + (improper_integral_+infty (f,b1))

improper_integral_+infty (f,b1) = +infty by A7, A9, A8, A3, A15, Th31;
then (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = +infty by A11, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) 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,b1)) + (improper_integral_+infty (f,b1))

improper_integral_+infty (f,b1) = -infty by A7, A9, A8, A3, A16, Th31;
then (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = -infty by A11, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) 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,b1)) + (improper_integral_+infty (f,b1))

A18: improper_integral_-infty (f,b1) = +infty by A1, A2, A17, A7, Lm4;

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,b1)) + (improper_integral_+infty (f,b1))

then A19: improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A3, Th27;
then improper_integral_+infty (f,b1) = (improper_integral_+infty (f,b)) + (integral (f,b1,b)) by A7, A9, A8, A3, Th31
.= (infty_ext_right_integral (f,b)) + (integral (f,b1,b)) by A19, XXREAL_3:def 2 ;
then (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = +infty by A18, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) 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,b1)) + (improper_integral_+infty (f,b1))

then improper_integral_+infty (f,b) = +infty by A17, A5, A3, Th27;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) by A17, A18, A7, A9, A8, A3, Th31; :: 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,b1)) + (improper_integral_+infty (f,b1))

A21: improper_integral_-infty (f,b1) = -infty by A1, A2, A20, A7, Lm5;

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,b1)) + (improper_integral_+infty (f,b1))

then A22: improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) by A3, Th27;
then improper_integral_+infty (f,b1) = (improper_integral_+infty (f,b)) + (integral (f,b1,b)) by A7, A9, A8, A3, Th31
.= (infty_ext_right_integral (f,b)) + (integral (f,b1,b)) by A22, XXREAL_3:def 2 ;
then (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = -infty by A21, XXREAL_3:def 2;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) 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,b1)) + (improper_integral_+infty (f,b1))

then improper_integral_+infty (f,b) = -infty by A20, A4, A3, Th27;
hence (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) by A20, A21, A7, A9, A8, A3, Th31; :: thesis: verum

end;

end;

end;

end;