let f be PartFunc of REAL,REAL; :: thesis:
let a, r be Real; :: thesis:
assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_improper_integrable_on a ; :: thesis:
A3: for d being Real st a <= d holds
( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded )

proof

let d be Real; :: thesis:
assume A4: a <= d ; :: thesis:
[.a,d.] c= [.a,+infty.[ by XXREAL_1:251;
then [.a,d.] c= dom f by A1;
then A5: ['a,d'] c= dom f by A4, INTEGRA5:def 3;
A6: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A2, A4;
hence r (#) f is_integrable_on ['a,d'] by A5, INTEGRA6:9; :: thesis:
thus (r (#) f) | ['a,d'] is bounded by A6, RFUNCT_1:80; :: thesis:

end;

per cases ;

suppose A7: f is_+infty_ext_Riemann_integrable_on a ; :: thesis:

then A8: improper_integral_+infty (f,a) = infty_ext_right_integral (f,a) by A2, Th27;
A9: ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) by A1, A7, INTEGR10:9;
thus r (#) f is_+infty_improper_integrable_on a by A1, A7, INTEGR10:9, Th21; :: thesis:
then improper_integral_+infty ((r (#) f),a) = infty_ext_right_integral ((r (#) f),a) by A9, Th27;
hence improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) by A8, A9, XXREAL_3:def 5; :: thesis:

end;

suppose A10: not f is_+infty_ext_Riemann_integrable_on a ; :: thesis:

consider Intf being PartFunc of REAL,REAL such that
A11: dom Intf = right_closed_halfline a and
A12: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) by A2;
A13: dom (r (#) Intf) = right_closed_halfline a by A11, VALUED_1:def 5;
A14: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),a,x)

proof

let x be Real; :: thesis:
assume A15: x in dom (r (#) Intf) ; :: thesis:
then A16: (r (#) Intf) . x = r * (Intf . x) by VALUED_1:def 5
.= r * (integral (f,a,x)) by A15, A13, A12, A11 ;
A17: a <= x by A13, A15, XXREAL_1:3;
[.a,x.] c= [.a,+infty.[ by XXREAL_1:251;
then [.a,x.] c= dom f by A1;
then A18: ['a,x'] c= dom f by A17, INTEGRA5:def 3;
( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A2, A17;
hence (r (#) Intf) . x = integral ((r (#) f),a,x) by A16, A17, A18, INTEGRA6:10; :: thesis:

end;

per cases by A2, A10, Th27;

suppose A19: improper_integral_+infty (f,a) = +infty ; :: thesis:

then A20: Intf is divergent_in+infty_to+infty by A2, A11, A12, Th39;

per cases ;

suppose A21: r > 0 ; :: thesis:

then A22: r (#) Intf is divergent_in+infty_to+infty by A19, A2, A11, A12, Th39, LIMFUNC1:58;
thus r (#) f is_+infty_improper_integrable_on a by A3, A13, A14, A21, A20, LIMFUNC1:58; :: thesis:
then improper_integral_+infty ((r (#) f),a) = +infty by A13, A14, A22, Def4;
hence improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) by A19, A21, XXREAL_3:def 5; :: thesis:

end;

suppose A23: r < 0 ; :: thesis:

then A24: r (#) Intf is divergent_in+infty_to-infty by A19, A2, A11, A12, Th39, LIMFUNC1:58;
thus r (#) f is_+infty_improper_integrable_on a by A3, A13, A14, A23, A20, LIMFUNC1:58; :: thesis:
then improper_integral_+infty ((r (#) f),a) = -infty by A13, A14, A24, Def4;
hence improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) by A19, A23, XXREAL_3:def 5; :: thesis:

end;

suppose A25: r = 0 ; :: thesis:

A26: for R being Real ex g being Real st
( R < g & g in dom (r (#) Intf) ) by A11, A13, A20, LIMFUNC1:46;
A27: for g1 being Real st 0 < g1 holds
ex R being Real st
for r1 being Real st R < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

proof

let g1 be Real; :: thesis:
assume A28: 0 < g1 ; :: thesis:

now :: thesis:

let r1 be Real; :: thesis:
assume ( a < r1 & r1 in dom (r (#) Intf) ) ; :: thesis:
then (r (#) Intf) . r1 = r * (Intf . r1) by VALUED_1:def 5
.= 0 by A25 ;
hence |.(((r (#) Intf) . r1) - 0).| < g1 by A28, ABSVALUE:2; :: thesis:

end;

hence ex R being Real st
for r1 being Real st R < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ; :: thesis:

end;

then A29: r (#) Intf is convergent_in+infty by A26, LIMFUNC1:44;
then A30: lim_in+infty (r (#) Intf) = 0 by A27, LIMFUNC1:79;
thus r (#) f is_+infty_improper_integrable_on a by A3, A13, A14, A27, A26, LIMFUNC1:44; :: thesis:
then improper_integral_+infty ((r (#) f),a) = 0 by A13, A14, A29, A30, Def4;
hence improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) by A25; :: thesis:

end;

suppose A31: improper_integral_+infty (f,a) = -infty ; :: thesis:

then A32: Intf is divergent_in+infty_to-infty by A2, A11, A12, Th40;

per cases ;

suppose A33: r > 0 ; :: thesis:

then A34: r (#) Intf is divergent_in+infty_to-infty by A31, A2, A11, A12, Th40, LIMFUNC1:58;
thus r (#) f is_+infty_improper_integrable_on a by A3, A13, A14, A33, A32, LIMFUNC1:58; :: thesis:
then improper_integral_+infty ((r (#) f),a) = -infty by A13, A14, A34, Def4;
hence improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) by A31, A33, XXREAL_3:def 5; :: thesis:

end;

suppose A35: r < 0 ; :: thesis:

then A36: r (#) Intf is divergent_in+infty_to+infty by A31, A2, A11, A12, Th40, LIMFUNC1:58;
thus r (#) f is_+infty_improper_integrable_on a by A3, A13, A14, A35, A32, LIMFUNC1:58; :: thesis:
then improper_integral_+infty ((r (#) f),a) = +infty by A13, A14, A36, Def4;
hence improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) by A31, A35, XXREAL_3:def 5; :: thesis:

end;

suppose A37: r = 0 ; :: thesis:

A38: for R being Real ex g being Real st
( R < g & g in dom (r (#) Intf) ) by A11, A13, A32, LIMFUNC1:47;
A39: for g1 being Real st 0 < g1 holds
ex R being Real st
for r1 being Real st R < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1

proof

let g1 be Real; :: thesis:
assume A40: 0 < g1 ; :: thesis:

now :: thesis:

let r1 be Real; :: thesis:
assume ( a < r1 & r1 in dom (r (#) Intf) ) ; :: thesis:
then (r (#) Intf) . r1 = r * (Intf . r1) by VALUED_1:def 5
.= 0 by A37 ;
hence |.(((r (#) Intf) . r1) - 0).| < g1 by A40, ABSVALUE:2; :: thesis:

end;

hence ex R being Real st
for r1 being Real st R < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ; :: thesis:

end;

then A41: r (#) Intf is convergent_in+infty by A38, LIMFUNC1:44;
then A42: lim_in+infty (r (#) Intf) = 0 by A39, LIMFUNC1:79;
thus r (#) f is_+infty_improper_integrable_on a by A3, A13, A14, A39, A38, LIMFUNC1:44; :: thesis:
then improper_integral_+infty ((r (#) f),a) = 0 by A13, A14, A41, A42, Def4;
hence improper_integral_+infty ((r (#) f),a) = r * (improper_integral_+infty (f,a)) by A37; :: thesis:

end;