let f be PartFunc of REAL , REAL ; :: thesis: for b being real number st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b holds
for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral (r (#) f),b = r * (infty_ext_left_integral f,b) )
let b be real number ; :: thesis: ( left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b implies for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral (r (#) f),b = r * (infty_ext_left_integral f,b) ) )
assume A1:
( left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b )
; :: thesis: for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral (r (#) f),b = r * (infty_ext_left_integral f,b) )
for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral (r (#) f),b = r * (infty_ext_left_integral f,b) )
proof
let r be
Real;
:: thesis: ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral (r (#) f),b = r * (infty_ext_left_integral f,b) )
consider Intf being
PartFunc of
REAL ,
REAL such that A2:
(
dom Intf = left_closed_halfline b & ( for
x being
Real st
x in dom Intf holds
Intf . x = integral f,
x,
b ) &
Intf is
convergent_in-infty &
infty_ext_left_integral f,
b = lim_in-infty Intf )
by Def8, A1;
set Intfg =
r (#) Intf;
A3:
for
a being
Real st
a <= b holds
(
r (#) f is_integrable_on ['a,b'] &
(r (#) f) | ['a,b'] is
bounded )
proof
let a be
Real;
:: thesis: ( a <= b implies ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) )
assume A4:
a <= b
;
:: thesis: ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded )
A5:
['a,b'] = [.a,b.]
by INTEGRA5:def 4, A4;
[.a,b.] c= left_closed_halfline b
by XXREAL_1:265;
then A6:
['a,b'] c= dom f
by A5, A1, XBOOLE_1:1;
A7:
(
f is_integrable_on ['a,b'] &
f | ['a,b'] is
bounded )
by A4, Def6, A1;
thus
(
r (#) f is_integrable_on ['a,b'] &
(r (#) f) | ['a,b'] is
bounded )
by A7, RFUNCT_1:97, A6, INTEGRA6:9;
:: thesis: verum
end;
A8:
(
dom (r (#) Intf) = left_closed_halfline 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) = left_closed_halfline 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 A10:
x in dom (r (#) Intf)
;
:: thesis: (r (#) Intf) . x = integral (r (#) f),x,b
then A11:
x <= b
by A9, XXREAL_1:234;
A12:
['x,b'] = [.x,b.]
by INTEGRA5:def 4, A11;
A13:
[.x,b.] c= left_closed_halfline b
by XXREAL_1:265;
A14:
(
f is_integrable_on ['x,b'] &
f | ['x,b'] is
bounded )
by A11, Def6, A1;
thus (r (#) Intf) . x =
r * (Intf . x)
by VALUED_1:def 5, A10
.=
r * (integral f,x,b)
by A2, A9, A10
.=
integral (r (#) f),
x,
b
by A13, A12, A1, XBOOLE_1:1, A14, INTEGRA6:10, A11
;
:: thesis: verum
end;
A15:
r (#) Intf is
convergent_in-infty
by A2, LIMFUNC1:124;
A16:
lim_in-infty (r (#) Intf) = r * (infty_ext_left_integral f,b)
by LIMFUNC1:124, A2;
thus
r (#) f is_-infty_ext_Riemann_integrable_on b
by A3, A8, A15, Def6;
:: thesis: infty_ext_left_integral (r (#) f),b = r * (infty_ext_left_integral f,b)
hence
infty_ext_left_integral (r (#) f),
b = r * (infty_ext_left_integral f,b)
by A8, A15, A16, Def8;
:: thesis: verum
end;
hence
for r being Real holds
( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral (r (#) f),b = r * (infty_ext_left_integral f,b) )
; :: thesis: verum