let f be PartFunc of REAL,REAL; for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) holds
( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) )
let a, b, c be Real; ( a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] & right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies ( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) )
assume that
A1:
( a <= b & b < c )
and
A2:
[.a,c.[ c= dom f
and
A3:
f | ['a,b'] is bounded
and
A4:
f is_right_improper_integrable_on b,c
and
A5:
f is_integrable_on ['a,b']
and
A6:
right_improper_integral (f,b,c) = ext_right_integral (f,b,c)
; ( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) )
consider I being PartFunc of REAL,REAL such that
A7:
dom I = [.b,c.[
and
A8:
for x being Real st x in dom I holds
I . x = integral (f,b,x)
and
A9:
( I is_left_convergent_in c or I is_left_divergent_to+infty_in c or I is_left_divergent_to-infty_in c )
by A4;
then
f is_right_ext_Riemann_integrable_on b,c
by A4, A7, A8, A9, A10, INTEGR10:def 1;
then A11:
( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (ext_right_integral (f,b,c)) + (integral (f,a,b)) )
by A1, A2, A3, A5, Th21;
ex Intf being PartFunc of REAL,REAL st
( dom Intf = [.a,c.[ & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in c )
by A11, INTEGR10:def 1;
hence
f is_right_improper_integrable_on a,c
by A1, A2, A3, A4, A5, Lm19; right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b))
then
right_improper_integral (f,a,c) = (ext_right_integral (f,b,c)) + (integral (f,a,b))
by A11, Th39;
hence
right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b))
by A6, XXREAL_3:def 2; verum