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

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

end;

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

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),a,x)) - (I2 . x) by A6, A20, A7, A8, A18;
then A21: (I1 - I2) . x = (integral ((max+ f),a,x)) - (integral ((max- f),a,x)) by A6, A20, A10, A11, A18;
A22: ( a <= x & x < +infty ) by A20, A18, XXREAL_1:3;
then ['a,x'] = [.a,x.] by INTEGRA5:def 3;
then ['a,x'] c= [.a,+infty.[ by A22, XXREAL_1:43;
then ['a,x'] c= dom f by A1, A6;
then A23: ( ['a,x'] c= dom (max+ f) & ['a,x'] c= dom (max- f) ) by RFUNCT_3:def 10, RFUNCT_3:def 11;
( max+ f is_integrable_on ['a,x'] & (max+ f) | ['a,x'] is bounded & max- f is_integrable_on ['a,x'] & (max- f) | ['a,x'] is bounded ) by A22, A2, A3, INTEGR10:def 5;
hence (I1 - I2) . x = integral (f,a,x) by A21, A22, A23, A13, INTEGRA6:12; :: thesis:

end;

A24: for r being Real ex g being Real st
( r < g & g in dom (I1 - I2) ) by A18, A6, A7, A9, LIMFUNC1:44;
hence f is_+infty_ext_Riemann_integrable_on a by A6, A14, A18, A19, A9, A12, LIMFUNC1:83, INTEGR10:def 5; :: thesis:
A25: ( I1 - I2 is convergent_in+infty & lim_in+infty (I1 - I2) = (lim_in+infty I1) - (lim_in+infty I2) ) by A24, A9, A12, LIMFUNC1:83;
then A26: f is_+infty_improper_integrable_on a by A6, A14, A18, A19, INTEGR10:def 5, INTEGR25:21;
A27: ( lim_in+infty I1 = improper_integral_+infty ((max+ f),a) & lim_in+infty I2 = improper_integral_+infty ((max- f),a) ) by A4, A5, A7, A8, A9, A10, A11, A12, INTEGR25:def 4;
then A28: - (lim_in+infty I2) = - (improper_integral_+infty ((max- f),a)) by XXREAL_3:def 3;
(improper_integral_+infty ((max+ f),a)) - (improper_integral_+infty ((max- f),a)) = (improper_integral_+infty ((max+ f),a)) + (- (improper_integral_+infty ((max- f),a))) 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,a) = (improper_integral_+infty ((max+ f),a)) - (improper_integral_+infty ((max- f),a)) by A26, A6, A18, A19, A25, INTEGR25:def 4; :: thesis: