let f be PartFunc of REAL,REAL; :: thesis: for b being Real st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b holds
for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) )
let b be Real; :: thesis: ( left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b implies for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) )
assume that
A1: left_closed_halfline b c= dom f and
A2: f is_-infty_ext_Riemann_integrable_on b ; :: thesis: for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) )
for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) )

proof

let r be Real; :: thesis: ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) )
consider Intf being PartFunc of REAL,REAL such that
A3: dom Intf = left_closed_halfline b and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A5: Intf is convergent_in-infty and
A6: infty_ext_left_integral (f,b) = lim_in-infty Intf by A2, Def8;
set Intfg = r (#) Intf;
A7: r (#) Intf is convergent_in-infty by A5, LIMFUNC1:89;
A8: ( dom (r (#) Intf) = left_closed_halfline b & ( for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b) ) )

proof

thus A9: dom (r (#) Intf) = left_closed_halfline b by A3, VALUED_1:def 5; :: thesis: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b)
let x be Real; :: thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),x,b) )
assume A10: x in dom (r (#) Intf) ; :: thesis: (r (#) Intf) . x = integral ((r (#) f),x,b)
then A11: x <= b by A9, XXREAL_1:234;
then A12: ( ['x,b'] = [.x,b.] & f is_integrable_on ['x,b'] ) by A2, INTEGRA5:def 3;
A13: ( [.x,b.] c= left_closed_halfline b & f | ['x,b'] is bounded ) by A2, A11, XXREAL_1:265;
thus (r (#) Intf) . x = r * (Intf . x) by A10, VALUED_1:def 5
.= r * (integral (f,x,b)) by A3, A4, A9, A10
.= integral ((r (#) f),x,b) by A1, A11, A12, A13, INTEGRA6:10, XBOOLE_1:1 ; :: thesis: verum

end;

for a being Real st a <= b holds
( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )

proof

let a be Real; :: thesis: ( a <= b implies ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) )
A14: [.a,b.] c= left_closed_halfline b by XXREAL_1:265;
assume A15: a <= b ; :: thesis: ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )
then A16: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A2;
['a,b'] = [.a,b.] by A15, INTEGRA5:def 3;
then ['a,b'] c= dom f by A1, A14;
hence ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) by A16, INTEGRA6:9, RFUNCT_1:80; :: thesis: verum

end;

hence A17: r (#) f is_-infty_ext_Riemann_integrable_on b by A8, A7; :: thesis: infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b))
lim_in-infty (r (#) Intf) = r * (infty_ext_left_integral (f,b)) by A5, A6, LIMFUNC1:89;
hence infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) by A8, A7, A17, Def8; :: thesis: verum

end;

hence for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) ; :: thesis: verum