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