let f be PartFunc of REAL ,REAL ; :: thesis: for a, b being Real st a < b & ['a,b'] c= dom f & f is_right_ext_Riemann_integrable_on a,b holds
for r being Real holds
( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b) )
let a, b be Real; :: thesis: ( a < b & ['a,b'] c= dom f & f is_right_ext_Riemann_integrable_on a,b implies for r being Real holds
( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b) ) )
assume that
A1: a < b and
A2: ['a,b'] c= dom f and
A3: f is_right_ext_Riemann_integrable_on a,b ; :: thesis: for r being Real holds
( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b) )
for r being Real holds
( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b) )

proof

let r be Real; :: thesis: ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b) )
consider Intf being PartFunc of REAL ,REAL such that
A4: dom Intf = [.a,b.[ and
A5: for x being Real st x in dom Intf holds
Intf . x = integral f,a,x and
A6: Intf is_left_convergent_in b and
A7: ext_right_integral f,a,b = lim_left Intf,b by A3, Def3;
set Intfg = r (#) Intf;
A8: r (#) Intf is_left_convergent_in b by A6, LIMFUNC2:51;
A9: ( dom (r (#) Intf) = [.a,b.[ & ( for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral (r (#) f),a,x ) )

proof

A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
thus A11: dom (r (#) Intf) = [.a,b.[ by A4, VALUED_1:def 5; :: 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 A12: x in dom (r (#) Intf) ; :: thesis: (r (#) Intf) . x = integral (r (#) f),a,x
then A13: a <= x by A11, XXREAL_1:3;
then A14: ['a,x'] = [.a,x.] by INTEGRA5:def 4;
A15: x < b by A11, A12, XXREAL_1:3;
then A16: [.a,x.] c= [.a,b.] by XXREAL_1:34;
A17: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A13, A15, Def1;
thus (r (#) Intf) . x = r * (Intf . x) by A12, VALUED_1:def 5
.= r * (integral f,a,x) by A4, A5, A11, A12
.= integral (r (#) f),a,x by A2, A13, A14, A10, A16, A17, INTEGRA6:10, XBOOLE_1:1 ; :: thesis: verum

end;

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

proof

let d be Real; :: thesis: ( a <= d & d < b implies ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) )
assume A18: ( a <= d & d < b ) ; :: thesis: ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded )
then A19: ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.] ) by INTEGRA5:def 4, XXREAL_1:34;
A20: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A3, A18, Def1;
['a,b'] = [.a,b.] by A1, INTEGRA5:def 4;
then ['a,d'] c= dom f by A2, A19, XBOOLE_1:1;
hence ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) by A20, INTEGRA6:9, RFUNCT_1:97; :: thesis: verum

end;

hence A21: r (#) f is_right_ext_Riemann_integrable_on a,b by A9, A8, Def1; :: thesis: ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b)
lim_left (r (#) Intf),b = r * (ext_right_integral f,a,b) by A6, A7, LIMFUNC2:51;
hence ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b) by A9, A8, A21, Def3; :: thesis: verum

end;

hence for r being Real holds
( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b) ) ; :: thesis: verum