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

proof

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

end;

per cases ;

suppose A8: f is_left_ext_Riemann_integrable_on a,b ; :: thesis:

then A9: left_improper_integral (f,a,b) = ext_left_integral (f,a,b) by A3, Th34;
A10: ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) by A2, A8, Th30;
thus r (#) f is_left_improper_integrable_on a,b by A2, A8, Th30, Th32; :: thesis:
then left_improper_integral ((r (#) f),a,b) = ext_left_integral ((r (#) f),a,b) by A10, Th34;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A9, A10, XXREAL_3:def 5; :: thesis:

end;

suppose A11: not f is_left_ext_Riemann_integrable_on a,b ; :: thesis:

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

proof

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

end;

per cases by A3, A11, Th34;

suppose A20: left_improper_integral (f,a,b) = +infty ; :: thesis:

then A21: Intf is_right_divergent_to+infty_in a by A3, A12, A13, Th49;

per cases ;

suppose A22: r > 0 ; :: thesis:

then A23: r (#) Intf is_right_divergent_to+infty_in a by A20, A3, A12, A13, Th49, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A22, A21, LIMFUNC2:22; :: thesis:
then left_improper_integral ((r (#) f),a,b) = +infty by A14, A15, A23, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A20, A22, XXREAL_3:def 5; :: thesis:

end;

suppose A24: r < 0 ; :: thesis:

then A25: r (#) Intf is_right_divergent_to-infty_in a by A20, A3, A12, A13, Th49, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A24, A21, LIMFUNC2:22; :: thesis:
then left_improper_integral ((r (#) f),a,b) = -infty by A14, A15, A25, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A20, A24, XXREAL_3:def 5; :: thesis:

end;

suppose A26: r = 0 ; :: thesis:

A27: for R being Real st a < R holds
ex g being Real st
( g < R & a < g & g in dom (r (#) Intf) ) by A12, A14, A21, LIMFUNC2:11;
A28: for g1 being Real st 0 < g1 holds
ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ) )

proof

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

now :: thesis:

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

end;

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

end;

then A30: r (#) Intf is_right_convergent_in a by A27, LIMFUNC2:10;
then A31: lim_right ((r (#) Intf),a) = 0 by A28, LIMFUNC2:42;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A28, A27, LIMFUNC2:10; :: thesis:
then left_improper_integral ((r (#) f),a,b) = 0 by A14, A15, A30, A31, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A26; :: thesis:

end;

suppose A32: left_improper_integral (f,a,b) = -infty ; :: thesis:

then A33: Intf is_right_divergent_to-infty_in a by A3, A12, A13, Th50;

per cases ;

suppose A34: r > 0 ; :: thesis:

then A35: r (#) Intf is_right_divergent_to-infty_in a by A32, A3, A12, A13, Th50, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A34, A33, LIMFUNC2:22; :: thesis:
then left_improper_integral ((r (#) f),a,b) = -infty by A14, A15, A35, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A32, A34, XXREAL_3:def 5; :: thesis:

end;

suppose A36: r < 0 ; :: thesis:

then A37: r (#) Intf is_right_divergent_to+infty_in a by A32, A3, A12, A13, Th50, LIMFUNC2:22;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A36, A33, LIMFUNC2:22; :: thesis:
then left_improper_integral ((r (#) f),a,b) = +infty by A14, A15, A37, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A32, A36, XXREAL_3:def 5; :: thesis:

end;

suppose A38: r = 0 ; :: thesis:

A39: for R being Real st a < R holds
ex g being Real st
( g < R & a < g & g in dom (r (#) Intf) ) by A12, A14, A33, LIMFUNC2:12;
A40: for g1 being Real st 0 < g1 holds
ex R being Real st
( a < R & ( for r1 being Real st r1 < R & a < r1 & r1 in dom (r (#) Intf) holds
|.(((r (#) Intf) . r1) - 0).| < g1 ) )

proof

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

now :: thesis:

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

end;

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

end;

then A42: r (#) Intf is_right_convergent_in a by A39, LIMFUNC2:10;
then A43: lim_right ((r (#) Intf),a) = 0 by A40, LIMFUNC2:42;
thus r (#) f is_left_improper_integrable_on a,b by A4, A14, A15, A40, A39, LIMFUNC2:10; :: thesis:
then left_improper_integral ((r (#) f),a,b) = 0 by A14, A15, A42, A43, Def3;
hence left_improper_integral ((r (#) f),a,b) = r * (left_improper_integral (f,a,b)) by A38; :: thesis:

end;