let f be PartFunc of REAL ,REAL ; :: thesis: for a, b being Real st a < b & ['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 & ['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 A1:
( a < b & ['a,b'] c= dom f & 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 A2:
(
dom Intf = ].a,b.] & ( for
x being
Real st
x in dom Intf holds
Intf . x = integral f,
x,
b ) &
Intf is_right_convergent_in a &
ext_left_integral f,
a,
b = lim_right Intf,
a )
by Def4, A1;
set Intfg =
r (#) Intf;
A3:
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 A4:
(
a < d &
d <= b )
;
:: thesis: ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded )
A5:
['d,b'] = [.d,b.]
by INTEGRA5:def 4, A4;
A6:
['a,b'] = [.a,b.]
by INTEGRA5:def 4, A1;
[.d,b.] c= [.a,b.]
by A4, XXREAL_1:34;
then A7:
['d,b'] c= dom f
by A6, A5, A1, XBOOLE_1:1;
A8:
(
f is_integrable_on ['d,b'] &
f | ['d,b'] is
bounded )
by A4, Def2, A1;
thus
(
r (#) f is_integrable_on ['d,b'] &
(r (#) f) | ['d,b'] is
bounded )
by A7, A8, INTEGRA6:9, RFUNCT_1:97;
:: thesis: verum
end;
A9:
(
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 A10:
dom (r (#) Intf) = ].a,b.]
by A2, 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 A11:
x in dom (r (#) Intf)
;
:: thesis: (r (#) Intf) . x = integral (r (#) f),x,b
then A12:
(
a < x &
x <= b )
by A10, XXREAL_1:2;
A13:
['x,b'] = [.x,b.]
by INTEGRA5:def 4, A12;
A14:
['a,b'] = [.a,b.]
by INTEGRA5:def 4, A1;
A15:
[.x,b.] c= [.a,b.]
by A12, XXREAL_1:34;
A16:
(
f is_integrable_on ['x,b'] &
f | ['x,b'] is
bounded )
by A12, Def2, A1;
thus (r (#) Intf) . x =
r * (Intf . x)
by VALUED_1:def 5, A11
.=
r * (integral f,x,b)
by A2, A10, A11
.=
integral (r (#) f),
x,
b
by A15, A14, A13, A1, XBOOLE_1:1, A16, INTEGRA6:10, A12
;
:: thesis: verum
end;
A17:
r (#) Intf is_right_convergent_in a
by A2, LIMFUNC2:60;
A18:
lim_right (r (#) Intf),
a = r * (ext_left_integral f,a,b)
by A2, LIMFUNC2:60;
thus
r (#) f is_left_ext_Riemann_integrable_on a,
b
by A3, A9, A17, Def2;
:: thesis: ext_left_integral (r (#) f),a,b = r * (ext_left_integral f,a,b)
hence
ext_left_integral (r (#) f),
a,
b = r * (ext_left_integral f,a,b)
by A9, A17, A18, Def4;
:: 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