let f be PartFunc of REAL,REAL; :: thesis:
let b be Real; :: thesis:
assume that
A1: left_closed_halfline b c= dom f and
A2: max+ f is_-infty_ext_Riemann_integrable_on b and
A3: max- f is_-infty_ext_Riemann_integrable_on b ; :: thesis:
A4: max+ f is_-infty_improper_integrable_on b by A2, INTEGR25:20;
A5: max- f is_-infty_improper_integrable_on b by A3, INTEGR25:20;
A6: left_closed_halfline b = ].-infty,b.] by LIMFUNC1:def 1;
consider I1 being PartFunc of REAL,REAL such that
A7: dom I1 = left_closed_halfline b and
A8: for x being Real st x in dom I1 holds
I1 . x = integral ((max+ f),x,b) and
A9: I1 is convergent_in-infty by A2, INTEGR10:def 6;
consider I2 being PartFunc of REAL,REAL such that
A10: dom I2 = left_closed_halfline b and
A11: for x being Real st x in dom I2 holds
I2 . x = integral ((max- f),x,b) and
A12: I2 is convergent_in-infty by A3, INTEGR10:def 6;
A13: f = (max+ f) - (max- f) by RFUNCT_3:34;
A14: for d being Real st d <= b holds
( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded )

let d be Real; :: thesis:
assume A15: d <= b ; :: thesis:
then A16: ( max+ f is_integrable_on ['d,b'] & (max+ f) | ['d,b'] is bounded & max- f is_integrable_on ['d,b'] & (max- f) | ['d,b'] is bounded ) by A2, A3, INTEGR10:def 6;
A17: d in REAL by XREAL_0:def 1;
['d,b'] = [.d,b.] by A15, INTEGRA5:def 3;
then ['d,b'] c= ].-infty,b.] by A17, XXREAL_0:12, XXREAL_1:39;
then ['d,b'] c= dom f by A1, A6;
then ( ['d,b'] c= dom (max+ f) & ['d,b'] c= dom (max- f) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
hence f is_integrable_on ['d,b'] by A13, A16, INTEGRA6:11; :: thesis:
f | (['d,b'] /\ ['d,b']) is bounded by A13, A16, RFUNCT_1:84;
hence f | ['d,b'] is bounded ; :: thesis:

end;

A18: dom (I1 - I2) = ].-infty,b.] /\ ].-infty,b.] by A6, A7, A10, VALUED_1:12;
A19: for x being Real st x in dom (I1 - I2) holds
(I1 - I2) . x = integral (f,x,b)

let x be Real; :: thesis:
assume A20: x in dom (I1 - I2) ; :: thesis:
then (I1 - I2) . x = (I1 . x) - (I2 . x) by VALUED_1:13;
then (I1 - I2) . x = (integral ((max+ f),x,b)) - (I2 . x) by A6, A20, A7, A8, A18;
then A21: (I1 - I2) . x = (integral ((max+ f),x,b)) - (integral ((max- f),x,b)) by A6, A20, A10, A11, A18;
A22: ( -infty < x & x <= b ) by A20, A18, XXREAL_1:2;
then ['x,b'] = [.x,b.] by INTEGRA5:def 3;
then ['x,b'] c= ].-infty,b.] by A22, XXREAL_1:39;
then ['x,b'] c= dom f by A1, A6;
then A23: ( ['x,b'] c= dom (max+ f) & ['x,b'] c= dom (max- f) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
( max+ f is_integrable_on ['x,b'] & (max+ f) | ['x,b'] is bounded & max- f is_integrable_on ['x,b'] & (max- f) | ['x,b'] is bounded ) by A22, A2, A3, INTEGR10:def 6;
hence (I1 - I2) . x = integral (f,x,b) by A21, A22, A23, A13, INTEGRA6:12; :: thesis:

end;

A24: for r being Real ex g being Real st
( g < r & g in dom (I1 - I2) ) by A18, A6, A7, A9, LIMFUNC1:45;
hence f is_-infty_ext_Riemann_integrable_on b by A6, A14, A18, A19, A9, A12, LIMFUNC1:92, INTEGR10:def 6; :: thesis:
A25: ( I1 - I2 is convergent_in-infty & lim_in-infty (I1 - I2) = (lim_in-infty I1) - (lim_in-infty I2) ) by A9, A12, A24, LIMFUNC1:92;
then A26: f is_-infty_improper_integrable_on b by A6, A14, A18, A19, INTEGR10:def 6, INTEGR25:20;
A27: ( lim_in-infty I1 = improper_integral_-infty ((max+ f),b) & lim_in-infty I2 = improper_integral_-infty ((max- f),b) ) by A4, A5, A7, A8, A9, A10, A11, A12, INTEGR25:def 3;
then A28: - (lim_in-infty I2) = - (improper_integral_-infty ((max- f),b)) by XXREAL_3:def 3;
(improper_integral_-infty ((max+ f),b)) - (improper_integral_-infty ((max- f),b)) = (improper_integral_-infty ((max+ f),b)) + (- (improper_integral_-infty ((max- f),b))) by XXREAL_3:def 4
.= (lim_in-infty I1) + (- (lim_in-infty I2)) by A27, A28, XXREAL_3:def 2 ;
hence improper_integral_-infty (f,b) = (improper_integral_-infty ((max+ f),b)) - (improper_integral_-infty ((max- f),b)) by A26, A6, A18, A19, A25, INTEGR25:def 3; :: thesis: