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