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 A1:
( a < b & ['a,b'] c= dom f & 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 A2:
(
dom Intf = [.a,b.[ & ( for
x being
Real st
x in dom Intf holds
Intf . x = integral f,
a,
x ) &
Intf is_left_convergent_in b &
ext_right_integral f,
a,
b = lim_left Intf,
b )
by Def3, A1;
set Intfg =
r (#) Intf;
R1:
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 A3:
(
a <= d &
d < b )
;
:: thesis: ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded )
A4:
['a,d'] = [.a,d.]
by INTEGRA5:def 4, A3;
A5:
['a,b'] = [.a,b.]
by INTEGRA5:def 4, A1;
[.a,d.] c= [.a,b.]
by A3, XXREAL_1:34;
then A6:
['a,d'] c= dom f
by A5, A4, A1, XBOOLE_1:1;
(
f is_integrable_on ['a,d'] &
f | ['a,d'] is
bounded )
by A3, Def1, A1;
hence
(
r (#) f is_integrable_on ['a,d'] &
(r (#) f) | ['a,d'] is
bounded )
by RFUNCT_1:97, A6, INTEGRA6:9;
:: thesis: verum
end;
A8:
(
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
thus A9:
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),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 &
x < b )
by A9, XXREAL_1:3;
A12:
['a,x'] = [.a,x.]
by INTEGRA5:def 4, A11;
A13:
['a,b'] = [.a,b.]
by INTEGRA5:def 4, A1;
A14:
[.a,x.] c= [.a,b.]
by A11, XXREAL_1:34;
A15:
(
f is_integrable_on ['a,x'] &
f | ['a,x'] is
bounded )
by A11, Def1, A1;
thus (r (#) Intf) . x =
r * (Intf . x)
by VALUED_1:def 5, A10
.=
r * (integral f,a,x)
by A2, A9, A10
.=
integral (r (#) f),
a,
x
by A13, A12, A1, XBOOLE_1:1, A14, A15, A11, INTEGRA6:10
;
:: thesis: verum
end;
A16:
r (#) Intf is_left_convergent_in b
by A2, LIMFUNC2:51;
A17:
lim_left (r (#) Intf),
b = r * (ext_right_integral f,a,b)
by A2, LIMFUNC2:51;
thus
r (#) f is_right_ext_Riemann_integrable_on a,
b
by R1, A8, A16, Def1;
:: thesis: ext_right_integral (r (#) f),a,b = r * (ext_right_integral f,a,b)
hence
ext_right_integral (r (#) f),
a,
b = r * (ext_right_integral f,a,b)
by A8, A16, A17, 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