let f be PartFunc of REAL,REAL; :: thesis: for a, b being Real st ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds
for r being Real holds
( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) )
let a, b be Real; :: thesis: ( ].a,b.] c= dom f & f is_left_ext_Riemann_integrable_on a,b implies for r being Real holds
( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) )
assume that
A1: ].a,b.] c= dom f and
A2: f is_left_ext_Riemann_integrable_on a,b ; :: thesis: for r being Real holds
( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) )
for r being Real holds
( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) )

proof

let r be Real; :: thesis: ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) )
consider Intf being PartFunc of REAL,REAL such that
A3: dom Intf = ].a,b.] and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) and
A5: Intf is_right_convergent_in a and
A6: ext_left_integral (f,a,b) = lim_right (Intf,a) by A2, INTEGR10:def 4;
set Intfg = r (#) Intf;
A7: r (#) Intf is_right_convergent_in a by A5, LIMFUNC2:52;
A8: ( dom (r (#) Intf) = ].a,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) = ].a,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: a < x by A9, XXREAL_1:2;
then A12: [.x,b.] c= ].a,b.] by XXREAL_1:39;
A13: x <= b by A9, A10, XXREAL_1:2;
then A14: ['x,b'] = [.x,b.] by INTEGRA5:def 3;
A15: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A2, A11, A13, INTEGR10:def 2;
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, A13, A14, A12, A15, INTEGRA6:10, XBOOLE_1:1 ; :: thesis: verum

end;

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: ( a < d & d <= b implies ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) )
assume A16: ( a < d & d <= b ) ; :: thesis: ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded )
then A17: ( ['d,b'] = [.d,b.] & [.d,b.] c= ].a,b.] ) by INTEGRA5:def 3, XXREAL_1:39;
A18: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A2, A16, INTEGR10:def 2;
['d,b'] c= dom f by A1, A17;
hence ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) by A18, INTEGRA6:9, RFUNCT_1:80; :: thesis: verum

end;

hence A19: r (#) f is_left_ext_Riemann_integrable_on a,b by A8, A5, LIMFUNC2:52, INTEGR10:def 2; :: thesis: ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b))
lim_right ((r (#) Intf),a) = r * (ext_left_integral (f,a,b)) by A5, A6, LIMFUNC2:52;
hence ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) by A8, A7, A19, INTEGR10:def 4; :: thesis: verum

end;

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