let f be PartFunc of REAL,REAL; :: thesis: for b being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )
let b be Real; :: thesis: ( dom f = REAL & f is_improper_integrable_on_REAL implies ( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) ) )
assume that
A1: dom f = REAL and
A2: f is_improper_integrable_on_REAL ; :: thesis: ( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )
consider b1 being Real such that
A3: f is_-infty_improper_integrable_on b1 and
A4: f is_+infty_improper_integrable_on b1 and
A5: improper_integral_on_REAL f = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) by A1, A2, Def6;

per cases ( b < b1 or b >= b1 ) ;

suppose A6: b < b1 ; :: thesis: ( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )

hence f is_-infty_improper_integrable_on b by A3, A1, Th25; :: thesis: ( f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )
A7: right_closed_halfline b c= dom f by A1;
( f | ['b,b1'] is bounded & f is_integrable_on ['b,b1'] ) by A3, A6;
hence f is_+infty_improper_integrable_on b by A6, A4, A7, Th31; :: thesis: improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b))
thus improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) by A1, A2, A5, Th35; :: thesis: verum

end;

suppose A8: b >= b1 ; :: thesis: ( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )

A9: left_closed_halfline b c= dom f by A1;
( f | ['b1,b'] is bounded & f is_integrable_on ['b1,b'] ) by A4, A8;
hence f is_-infty_improper_integrable_on b by A3, A8, A9, Th26; :: thesis: ( f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )
thus f is_+infty_improper_integrable_on b by A8, A1, A4, Th30; :: thesis: improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b))
thus improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) by A1, A2, A5, Th35; :: thesis: verum

end;

end;