let f be PartFunc of REAL,REAL; :: thesis: for a being Real st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a holds
for r being Real holds
( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * () )

let a be Real; :: thesis: ( right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a implies for r being Real holds
( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * () ) )

assume that
A1: right_closed_halfline a c= dom f and
A2: f is_+infty_ext_Riemann_integrable_on a ; :: thesis: for r being Real holds
( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * () )

for r being Real holds
( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * () )
proof
let r be Real; :: thesis: ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * () )
consider Intf being PartFunc of REAL,REAL such that
A3: dom Intf = right_closed_halfline a and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) and
A5: Intf is convergent_in+infty and
A6: infty_ext_right_integral (f,a) = lim_in+infty Intf by ;
set Intfg = r (#) Intf;
A7: r (#) Intf is convergent_in+infty by ;
A8: ( dom (r (#) Intf) = right_closed_halfline a & ( for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),a,x) ) )
proof
thus A9: dom (r (#) Intf) = right_closed_halfline a by ; :: thesis: for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),a,x)

let x be Real; :: thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),a,x) )
assume A10: x in dom (r (#) Intf) ; :: thesis: (r (#) Intf) . x = integral ((r (#) f),a,x)
then A11: a <= x by ;
then A12: ( ['a,x'] = [.a,x.] & f is_integrable_on ['a,x'] ) by ;
A13: ( [.a,x.] c= right_closed_halfline a & f | ['a,x'] is bounded ) by ;
thus (r (#) Intf) . x = r * (Intf . x) by
.= r * (integral (f,a,x)) by A3, A4, A9, A10
.= integral ((r (#) f),a,x) by ; :: thesis: verum
end;
for b being Real st a <= b holds
( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )
proof
let b be Real; :: thesis: ( a <= b implies ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) )
A14: [.a,b.] c= right_closed_halfline a by XXREAL_1:251;
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 ;
then ['a,b'] c= dom f by ;
hence ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) by ; :: thesis: verum
end;
hence A17: r (#) f is_+infty_ext_Riemann_integrable_on a by A8, A7; :: thesis: infty_ext_right_integral ((r (#) f),a) = r * ()
lim_in+infty (r (#) Intf) = r * () by ;
hence infty_ext_right_integral ((r (#) f),a) = r * () by A8, A7, A17, Def7; :: thesis: verum
end;
hence for r being Real holds
( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * () ) ; :: thesis: verum