let f be PartFunc of REAL,REAL; 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; ( ].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
; 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;
( 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;
for x being Real st x in dom (r (#) Intf) holds
(r (#) Intf) . x = integral ((r (#) f),x,b)
let x be
Real;
( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),x,b) )
assume A10:
x in dom (r (#) Intf)
;
(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
;
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;
( a < d & d <= b implies ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) )
assume A16:
(
a < d &
d <= b )
;
( 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;
verum
end;
hence A19:
r (#) f is_left_ext_Riemann_integrable_on a,
b
by A8, A5, LIMFUNC2:52, INTEGR10:def 2;
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;
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)) )
; verum